1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl
  5  
  6  Theory of complete lattices.
  7  -/
  8  import order.bounded_lattice order.bounds data.set.basic tactic.pi_instances
src         └───────────────────┘ └──────────┘ └────────────┘ └─────────────────┘
  9  
 10  set_option old_structure_cmd true
doc             └───────────────┘
 11  open set
 12  
 13  namespace lattice
 14  universes u v w w₂
 15  variables {α : Type u} {β : Type v} {ι : Sort w} {ι₂ : Sort w₂}
 16  
 17  /-- class for the `Sup` operator -/
 18  class has_Sup (α : Type u) := (Sup : set α → α)
id                      └──┘              └─┘   
src                                       └─┘
typ                     └──┘              └─┘   
 19  /-- class for the `Inf` operator -/
 20  class has_Inf (α : Type u) := (Inf : set α → α)
id                      └──┘              └─┘   
src                                       └─┘
typ                     └──┘              └─┘   
 21  /-- Supremum of a set -/
 22  def Sup [has_Sup α] : set α → α := has_Sup.Sup
id            └─────┘     └─┘        └─────────┘
src           └─────┘      └─┘          └─────────┘
typ           └─────┘     └─┘        └─────────┘
doc           └─────┘
 23  /-- Infimum of a set -/
 24  def Inf [has_Inf α] : set α → α := has_Inf.Inf
id            └─────┘     └─┘        └─────────┘
src           └─────┘      └─┘          └─────────┘
typ           └─────┘     └─┘        └─────────┘
doc           └─────┘
 25  /-- Indexed supremum -/
 26  def supr [has_Sup α] (s : ι → α) : α := Sup (range s)
id             └─────┘                   └─┘  └───┘ 
src            └─────┘                       └─┘  └───┘
typ            └─────┘                   └─┘  └───┘ 
doc            └─────┘                       └─┘  └───┘
 27  /-- Indexed infimum -/
 28  def infi [has_Inf α] (s : ι → α) : α := Inf (range s)
id             └─────┘                   └─┘  └───┘ 
src            └─────┘                       └─┘  └───┘
typ            └─────┘                   └─┘  └───┘ 
doc            └─────┘                       └─┘  └───┘
 29  
 30  lemma has_Inf_to_nonempty (α) [has_Inf α] : nonempty α := ⟨Inf ∅⟩
id                                  └─────┘     └──────┘      └─┘ 
src                                 └─────┘      └──────┘       └─┘ 
typ                                 └─────┘     └──────┘      └─┘ 
doc                                 └─────┘                     └─┘
 31  lemma has_Sup_to_nonempty (α) [has_Sup α] : nonempty α := ⟨Sup ∅⟩
id                                  └─────┘     └──────┘      └─┘ 
src                                 └─────┘      └──────┘       └─┘ 
typ                                 └─────┘     └──────┘      └─┘ 
doc                                 └─────┘                     └─┘
 32  
 33  notation `⨆` binders `, ` r:(scoped f, supr f) := r
id                                          └──┘
src                                         └──┘
typ                                         └──┘
doc                                         └──┘
 34  notation `⨅` binders `, ` r:(scoped f, infi f) := r
id                                          └──┘
src                                         └──┘
typ                                         └──┘
doc                                         └──┘
 35  
 36  section prio
 37  set_option default_priority 100 -- see Note [default priority]
doc             └──────────────┘
 38  /-- A complete lattice is a bounded lattice which
 39    has suprema and infima for every subset. -/
 40  class complete_lattice (α : Type u) extends bounded_lattice α, has_Sup α, has_Inf α :=
id                              └──┘            └─────────────┘   └─────┘   └─────┘ 
src                                              └─────────────┘    └─────┘    └─────┘
typ                             └──┘            └─────────────┘   └─────┘   └─────┘ 
doc                                              └─────────────┘    └─────┘    └─────┘
 41  (le_Sup : ∀s, ∀a∈s, a ≤ Sup s)
id                      └─┘ 
src                       
typ                     └─┘ 
 42  (Sup_le : ∀s a, (∀b∈s, b ≤ a) → Sup s ≤ a)
id                            └─┘   
src                                       
typ                           └─┘   
 43  (Inf_le : ∀s, ∀a∈s, Inf s ≤ a)
id                    └─┘   
src                            
typ                   └─┘   
 44  (le_Inf : ∀s a, (∀b∈s, a ≤ b) → a ≤ Inf s)
id                              └─┘ 
src                                   
typ                             └─┘ 
 45  
 46  /-- A complete linear order is a linear order whose lattice structure is complete. -/
 47  class complete_linear_order (α : Type u) extends complete_lattice α, decidable_linear_order α
id                                   └──┘            └──────────────┘   └────────────────────┘ 
src                                                   └──────────────┘    └────────────────────┘
typ                                  └──┘            └──────────────┘   └────────────────────┘ 
doc                                                   └──────────────┘
 48  end prio
 49  
 50  section
 51  variables [complete_lattice α] {s t : set α} {a b : α}
id              └──────────────┘           └─┘
src             └──────────────┘           └─┘
typ             └──────────────┘           └─┘
doc             └──────────────┘
 52  
 53  @[ematch] theorem le_Sup : a ∈ s → a ≤ Sup s := complete_lattice.le_Sup s a
id                                     └─┘     └─────────────────────┘  
src    └────┘                             └─┘      └─────────────────────┘
typ                                    └─┘     └─────────────────────┘  
doc    └────┘                               └─┘
 54  
 55  theorem Sup_le : (∀b∈s, b ≤ a) → Sup s ≤ a := complete_lattice.Sup_le s a
id                               └─┘       └─────────────────────┘  
src                                  └─┘         └─────────────────────┘
typ                              └─┘       └─────────────────────┘  
doc                                   └─┘
 56  
 57  @[ematch] theorem Inf_le : a ∈ s → Inf s ≤ a := complete_lattice.Inf_le s a
id                                   └─┘       └─────────────────────┘  
src    └────┘                          └─┘         └─────────────────────┘
typ                                  └─┘       └─────────────────────┘  
doc    └────┘                           └─┘
 58  
 59  theorem le_Inf : (∀b∈s, a ≤ b) → a ≤ Inf s := complete_lattice.le_Inf s a
id                                 └─┘     └─────────────────────┘  
src                                     └─┘      └─────────────────────┘
typ                                └─┘     └─────────────────────┘  
doc                                       └─┘
 60  
 61  lemma is_lub_Sup : is_lub s (Sup s) := ⟨assume x, le_Sup, assume x, Sup_le⟩
id                      └────┘   └─┘                └────┘           └────┘
src                     └────┘    └─┘                  └────┘            └────┘
typ                     └────┘   └─┘                └────┘           └────┘
doc                     └────┘    └─┘
 62  
 63  lemma is_lub_iff_Sup_eq : is_lub s a ↔ Sup s = a := is_lub_iff_eq_of_is_lub is_lub_Sup
id                             └────┘    └─┘       └─────────────────────┘ └────────┘
src                            └────┘      └─┘         └─────────────────────┘ └────────┘
typ                            └────┘    └─┘       └─────────────────────┘ └────────┘
doc                            └────┘       └─┘
 64  
 65  lemma is_glb_Inf : is_glb s (Inf s) := ⟨assume a, Inf_le, assume a, le_Inf⟩
id                      └────┘   └─┘                └────┘           └────┘
src                     └────┘    └─┘                  └────┘            └────┘
typ                     └────┘   └─┘                └────┘           └────┘
doc                     └────┘    └─┘
 66  
 67  lemma is_glb_iff_Inf_eq : is_glb s a ↔ Inf s = a := is_glb_iff_eq_of_is_glb is_glb_Inf
id                             └────┘    └─┘       └─────────────────────┘ └────────┘
src                            └────┘      └─┘         └─────────────────────┘ └────────┘
typ                            └────┘    └─┘       └─────────────────────┘ └────────┘
doc                            └────┘       └─┘
 68  
 69  theorem le_Sup_of_le (hb : b ∈ s) (h : a ≤ b) : a ≤ Sup s :=
id                                               └─┘ 
src                                                   └─┘
typ                                              └─┘ 
doc                                                      └─┘
 70  le_trans h (le_Sup hb)
id   └──────┘   └────┘ └┘
src  └──────┘    └────┘
typ  └──────┘   └────┘ └┘
 71  
 72  theorem Inf_le_of_le (hb : b ∈ s) (h : b ≤ a) : Inf s ≤ a :=
id                                             └─┘   
src                                                └─┘   
typ                                            └─┘   
doc                                                  └─┘
 73  le_trans (Inf_le hb) h
id   └──────┘  └────┘ └┘  
src  └──────┘  └────┘
typ  └──────┘  └────┘ └┘  
 74  
 75  theorem Sup_le_Sup (h : s ⊆ t) : Sup s ≤ Sup t :=
id                                 └─┘   └─┘ 
src                                  └─┘    └─┘
typ                                └─┘   └─┘ 
doc                                   └─┘     └─┘
 76  Sup_le (assume a, assume ha : a ∈ s, le_Sup $ h ha)
id   └────┘                           └────┘    └┘
src  └────┘                              └────┘
typ  └────┘                           └────┘    └┘
 77  
 78  theorem Inf_le_Inf (h : s ⊆ t) : Inf t ≤ Inf s :=
id                                 └─┘   └─┘ 
src                                  └─┘    └─┘
typ                                └─┘   └─┘ 
doc                                   └─┘     └─┘
 79  le_Inf (assume a, assume ha : a ∈ s, Inf_le $ h ha)
id   └────┘                           └────┘    └┘
src  └────┘                              └────┘
typ  └────┘                           └────┘    └┘
 80  
 81  @[simp] theorem Sup_le_iff : Sup s ≤ a ↔ (∀b ∈ s, b ≤ a) :=
id                                └─┘              
src                               └─┘                  
typ                               └─┘              
doc    └──┘                       └─┘
 82  ⟨assume : Sup s ≤ a, assume b, assume : b ∈ s,
id             └─┘                         
src            └─┘                            
typ            └─┘                         
doc            └─┘
 83    le_trans (le_Sup ‹b ∈ s›) ‹Sup s ≤ a›,
id     └──────┘  └────┘     └─┘   
src    └──────┘  └────┘       └─┘     
typ    └──────┘  └────┘     └─┘   
doc                            └─┘      
 84    Sup_le⟩
id     └────┘
src    └────┘
typ    └────┘
 85  
 86  @[simp] theorem le_Inf_iff : a ≤ Inf s ↔ (∀b ∈ s, a ≤ b) :=
id                                  └─┘            
src                                  └─┘               
typ                                 └─┘            
doc    └──┘                           └─┘
 87  ⟨assume : a ≤ Inf s, assume b, assume : b ∈ s,
id               └─┘                       
src               └─┘                         
typ              └─┘                       
doc                └─┘
 88    le_trans ‹a ≤ Inf s› (Inf_le ‹b ∈ s›),
id     └──────┘   └─┘   └────┘   
src    └──────┘    └─┘    └────┘     
typ    └──────┘   └─┘   └────┘   
doc                 └─┘                
 89    le_Inf⟩
id     └────┘
src    └────┘
typ    └────┘
 90  
 91  -- how to state this? instead a parameter `a`, use `∃a, a ∈ s` or `s ≠ ∅`?
 92  theorem Inf_le_Sup (h : a ∈ s) : Inf s ≤ Sup s :=
id                                 └─┘   └─┘ 
src                                  └─┘    └─┘
typ                                └─┘   └─┘ 
doc                                   └─┘     └─┘
 93  by have := le_Sup h; finish
id              └────┘ 
src     └──────┘└────┘   └──────
typ     └──────┘└────┘  └──────
doc     └──────┘         └──────
txt     └──────┘         └──────
par     └──────┘         └──────
pid     └───┘└─┘               
st     └─────────────────────────
 94  --Inf_le_of_le h (le_Sup h)
src  ────────────────────────────
typ  ────────────────────────────
doc  ────────────────────────────
txt  ────────────────────────────
par  ────────────────────────────
pid  ────────────────────────────
st   ────────────────────────────
 95  
src  
typ  
doc  
txt  
par  
pid  
st   
 96  -- TODO: it is weird that we have to add union_def
src  ──────────────────────────────────────────────────┘
typ  ──────────────────────────────────────────────────┘
doc  ──────────────────────────────────────────────────┘
txt  ──────────────────────────────────────────────────┘
par  ──────────────────────────────────────────────────┘
pid  ──────────────────────────────────────────────────┘
st   ──────────────────────────────────────────────────┘
 97  theorem Sup_union {s t : set α} : Sup (s ∪ t) = Sup s ⊔ Sup t :=
id                            └─┘     └─┘       └─┘   └─┘ 
src                           └─┘      └─┘         └─┘    └─┘
typ                           └─┘     └─┘       └─┘   └─┘ 
doc                                    └─┘           └─┘     └─┘
 98  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
 99    (by finish)
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
st        └─────┘
100    (sup_le (Sup_le_Sup $ subset_union_left _ _) (Sup_le_Sup $ subset_union_right _ _))
id      └────┘  └────────┘   └───────────────┘       └────────┘   └────────────────┘
src     └────┘  └────────┘   └───────────────┘       └────────┘   └────────────────┘
typ     └────┘  └────────┘   └───────────────┘       └────────┘   └────────────────┘
101  
102  /- old proof:
103  le_antisymm
104    (Sup_le $ assume a h, or.rec_on h (le_sup_left_of_le ∘ le_Sup) (le_sup_right_of_le ∘ le_Sup))
105    (sup_le (Sup_le_Sup $ subset_union_left _ _) (Sup_le_Sup $ subset_union_right _ _))
106  -/
107  
108  theorem Sup_inter_le {s t : set α} : Sup (s ∩ t) ≤ Sup s ⊓ Sup t :=
id                               └─┘     └─┘       └─┘   └─┘ 
src                              └─┘      └─┘         └─┘    └─┘
typ                              └─┘     └─┘       └─┘   └─┘ 
doc                                       └─┘           └─┘     └─┘
109  by finish
src     └──────
typ     └──────
doc     └──────
txt     └──────
par     └──────
pid           
st     └───────
110  /-
src  ───
typ  ───
doc  ───
txt  ───
par  ───
pid  ───
st   ───
111    Sup_le (assume a ⟨a_s, a_t⟩, le_inf (le_Sup a_s) (le_Sup a_t))
src  ─────────────────────────────────────────────────────────────────
typ  ─────────────────────────────────────────────────────────────────
doc  ─────────────────────────────────────────────────────────────────
txt  ─────────────────────────────────────────────────────────────────
par  ─────────────────────────────────────────────────────────────────
pid  ─────────────────────────────────────────────────────────────────
st   ─────────────────────────────────────────────────────────────────
112  -/
src  ───
typ  ───
doc  ───
txt  ───
par  ───
pid  ───
st   ───
113  
src  
typ  
doc  
txt  
par  
pid  
st   
114  theorem Inf_union {s t : set α} : Inf (s ∪ t) = Inf s ⊓ Inf t :=
id                            └─┘     └─┘       └─┘   └─┘ 
src                           └─┘      └─┘         └─┘    └─┘
typ                           └─┘     └─┘       └─┘   └─┘ 
doc                                    └─┘           └─┘     └─┘
115  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
116    (le_inf (Inf_le_Inf $ subset_union_left _ _) (Inf_le_Inf $ subset_union_right _ _))
id      └────┘  └────────┘   └───────────────┘       └────────┘   └────────────────┘
src     └────┘  └────────┘   └───────────────┘       └────────┘   └────────────────┘
typ     └────┘  └────────┘   └───────────────┘       └────────┘   └────────────────┘
117    (by finish)
src        └────┘
typ        └────┘
doc        └────┘
txt        └────┘
par        └────┘
st        └─────┘
118  
119  /- old proof:
120  le_antisymm
121    (le_inf (Inf_le_Inf $ subset_union_left _ _) (Inf_le_Inf $ subset_union_right _ _))
122    (le_Inf $ assume a h, or.rec_on h (inf_le_left_of_le ∘ Inf_le) (inf_le_right_of_le ∘ Inf_le))
123  -/
124  
125  theorem le_Inf_inter {s t : set α} : Inf s ⊔ Inf t ≤ Inf (s ∩ t) :=
id                               └─┘     └─┘   └─┘   └─┘    
src                              └─┘      └─┘    └─┘    └─┘    
typ                              └─┘     └─┘   └─┘   └─┘    
doc                                       └─┘     └─┘     └─┘
126  by finish
src     └──────
typ     └──────
doc     └──────
txt     └──────
par     └──────
pid           
st     └───────
127  /-
src  ───
typ  ───
doc  ───
txt  ───
par  ───
pid  ───
st   ───
128  le_Inf (assume a ⟨a_s, a_t⟩, sup_le (Inf_le a_s) (Inf_le a_t))
src  ───────────────────────────────────────────────────────────────
typ  ───────────────────────────────────────────────────────────────
doc  ───────────────────────────────────────────────────────────────
txt  ───────────────────────────────────────────────────────────────
par  ───────────────────────────────────────────────────────────────
pid  ───────────────────────────────────────────────────────────────
st   ───────────────────────────────────────────────────────────────
129  -/
src  ───
typ  ───
doc  ───
txt  ───
par  ───
pid  ───
st   ───
130  
src  
typ  
doc  
txt  
par  
pid  
st   
131  @[simp] theorem Sup_empty : Sup ∅ = (⊥ : α) :=
id                               └─┘       
src                              └─┘    
typ                              └─┘       
doc    └──┘                      └─┘
132  le_antisymm (by finish) (by finish)
id   └─────────┘
src  └─────────┘     └────┘      └────┘
typ  └─────────┘     └────┘      └────┘
doc                  └────┘      └────┘
txt                  └────┘      └────┘
par                  └────┘      └────┘
st                  └─────┘     └─────┘
133  -- le_antisymm (Sup_le (assume _, false.elim)) bot_le
134  
135  @[simp] theorem Inf_empty : Inf ∅ = (⊤ : α) :=
id                               └─┘       
src                              └─┘    
typ                              └─┘       
doc    └──┘                      └─┘
136  le_antisymm (by finish) (by finish)
id   └─────────┘
src  └─────────┘     └────┘      └────┘
typ  └─────────┘     └────┘      └────┘
doc                  └────┘      └────┘
txt                  └────┘      └────┘
par                  └────┘      └────┘
st                  └─────┘     └─────┘
137  --le_antisymm le_top (le_Inf (assume _, false.elim))
138  
139  @[simp] theorem Sup_univ : Sup univ = (⊤ : α) :=
id                              └─┘ └──┘      
src                             └─┘ └──┘   
typ                             └─┘ └──┘      
doc    └──┘                     └─┘
140  le_antisymm (by finish) (le_Sup ⟨⟩) -- finish fails because ⊤ ≤ a simplifies to a = ⊤
id   └─────────┘              └────┘ 
src  └─────────┘     └────┘   └────┘ 
typ  └─────────┘     └────┘   └────┘ 
doc                  └────┘
txt                  └────┘
par                  └────┘
st                  └─────┘
141  --le_antisymm le_top (le_Sup ⟨⟩)
142  
143  @[simp] theorem Inf_univ : Inf univ = (⊥ : α) :=
id                              └─┘ └──┘      
src                             └─┘ └──┘   
typ                             └─┘ └──┘      
doc    └──┘                     └─┘
144  le_antisymm (Inf_le ⟨⟩) bot_le
id   └─────────┘  └────┘    └────┘
src  └─────────┘  └────┘    └────┘
typ  └─────────┘  └────┘    └────┘
145  
146  -- TODO(Jeremy): get this automatically
147  @[simp] theorem Sup_insert {a : α} {s : set α} : Sup (insert a s) = a ⊔ Sup s :=
id                                          └─┘     └─┘  └────┘       └─┘ 
src                                          └─┘      └─┘  └────┘          └─┘
typ                                         └─┘     └─┘  └────┘       └─┘ 
doc    └──┘                                           └─┘                    └─┘
148  have Sup {b | b = a} = a,
id        └─┘         
src       └─┘           
typ       └─┘         
doc       └─┘
149    from le_antisymm (Sup_le $ assume b b_eq, b_eq ▸ le_refl _) (le_Sup rfl),
id          └─────────┘  └────┘           └──┘  └──┘  └─────┘     └────┘ └─┘
src         └─────────┘  └────┘                        └─────┘     └────┘ └─┘
typ         └─────────┘  └────┘           └──┘  └──┘  └─────┘     └────┘ └─┘
150  calc Sup (insert a s) = Sup {b | b = a} ⊔ Sup s : Sup_union
id        └─┘  └────┘      └─┘         └─┘    └───────┘
src       └─┘  └────┘        └─┘            └─┘     └───────┘
typ       └─┘  └────┘      └─┘         └─┘    └───────┘
doc       └─┘                └─┘               └─┘
151                    ... = a ⊔ Sup s : by rw [this]
id                             └─┘           └──┘
src                             └─┘        └──┘    └─
typ                            └─┘       └──┘└──┘└─
doc                              └─┘        └──┘    └─
txt                                         └──┘    └─
par                                         └──┘    └─
pid                                           └┘    
st                                         └───────┘
152  
src  
typ  
doc  
txt  
par  
pid  
st   
153  @[simp] theorem Inf_insert {a : α} {s : set α} : Inf (insert a s) = a ⊓ Inf s :=
id                                          └─┘     └─┘  └────┘       └─┘ 
src                                          └─┘      └─┘  └────┘          └─┘
typ                                         └─┘     └─┘  └────┘       └─┘ 
doc    └──┘                                           └─┘                    └─┘
154  have Inf {b | b = a} = a,
id        └─┘         
src       └─┘           
typ       └─┘         
doc       └─┘
155    from le_antisymm (Inf_le rfl) (le_Inf $ assume b b_eq, b_eq ▸ le_refl _),
id          └─────────┘  └────┘ └─┘   └────┘           └──┘  └──┘  └─────┘
src         └─────────┘  └────┘ └─┘   └────┘                        └─────┘
typ         └─────────┘  └────┘ └─┘   └────┘           └──┘  └──┘  └─────┘
156  calc Inf (insert a s) = Inf {b | b = a} ⊓ Inf s : Inf_union
id        └─┘  └────┘      └─┘         └─┘    └───────┘
src       └─┘  └────┘        └─┘            └─┘     └───────┘
typ       └─┘  └────┘      └─┘         └─┘    └───────┘
doc       └─┘                └─┘               └─┘
157                    ... = a ⊓ Inf s : by rw [this]
id                             └─┘           └──┘
src                             └─┘        └──┘    └─
typ                            └─┘       └──┘└──┘└─
doc                              └─┘        └──┘    └─
txt                                         └──┘    └─
par                                         └──┘    └─
pid                                           └┘    
st                                         └───────┘
158  
src  
typ  
doc  
txt  
par  
pid  
st   
159  @[simp] theorem Sup_singleton {a : α} : Sup {a} = a :=
id                                          └─┘    
src                                          └─┘    
typ                                         └─┘    
doc    └──┘                                  └─┘
160  by finish [singleton_def]
id              └───────────┘
src     └──────┘└───────────┘└─
typ     └──────┘└───────────┘└─
doc     └──────┘             └─
txt     └──────┘             └─
par     └──────┘             └─
pid           └┘             
st     └───────────────────────
161  --eq.trans Sup_insert $ by simp
src  ────────────────────────────────
typ  ────────────────────────────────
doc  ────────────────────────────────
txt  ────────────────────────────────
par  ────────────────────────────────
pid  ────────────────────────────────
st   ────────────────────────────────
162  
src  
typ  
doc  
txt  
par  
pid  
st   
163  @[simp] theorem Inf_singleton {a : α} : Inf {a} = a :=
id                                          └─┘    
src                                          └─┘    
typ                                         └─┘    
doc    └──┘                                  └─┘
164  by finish [singleton_def]
id              └───────────┘
src     └──────┘└───────────┘└─
typ     └──────┘└───────────┘└─
doc     └──────┘             └─
txt     └──────┘             └─
par     └──────┘             └─
pid           └┘             
st     └───────────────────────
165  --eq.trans Inf_insert $ by simp
src  ────────────────────────────────
typ  ────────────────────────────────
doc  ────────────────────────────────
txt  ────────────────────────────────
par  ────────────────────────────────
pid  ────────────────────────────────
st   ────────────────────────────────
166  
src  
typ  
doc  
txt  
par  
pid  
st   
167  @[simp] theorem Inf_eq_top : Inf s = ⊤ ↔ (∀a∈s, a = ⊤) :=
id                                └─┘            
src                               └─┘                
typ                               └─┘            
doc    └──┘                       └─┘
168  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
169    (assume h a ha, top_unique $ h ▸ Inf_le ha)
id               └┘  └────────┘     └────┘ └┘
src                    └────────┘      └────┘
typ              └┘  └────────┘     └────┘ └┘
170    (assume h, top_unique $ le_Inf $ assume a ha, top_le_iff.2 $ h a ha)
id               └────────┘   └────┘           └┘  └────────┘      └┘
src               └────────┘   └────┘                └────────┘
typ              └────────┘   └────┘           └┘  └────────┘      └┘
171  
172  @[simp] theorem Sup_eq_bot : Sup s = ⊥ ↔ (∀a∈s, a = ⊥) :=
id                                └─┘            
src                               └─┘                
typ                               └─┘            
doc    └──┘                       └─┘
173  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
174    (assume h a ha, bot_unique $ h ▸ le_Sup ha)
id               └┘  └────────┘     └────┘ └┘
src                    └────────┘      └────┘
typ              └┘  └────────┘     └────┘ └┘
175    (assume h, bot_unique $ Sup_le $ assume a ha, le_bot_iff.2 $ h a ha)
id               └────────┘   └────┘           └┘  └────────┘      └┘
src               └────────┘   └────┘                └────────┘
typ              └────────┘   └────┘           └┘  └────────┘      └┘
176  
177  end
178  
179  section complete_linear_order
180  variables [complete_linear_order α] {s t : set α} {a b : α}
id              └───────────────────┘           └─┘
src             └───────────────────┘           └─┘
typ             └───────────────────┘           └─┘
doc             └───────────────────┘
181  
182  lemma Inf_lt_iff : Inf s < b ↔ (∃a∈s, a < b) :=
id                      └─┘          
src                     └─┘              
typ                     └─┘          
doc                     └─┘
183  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
184    (assume : Inf s < b, classical.by_contradiction $ assume : ¬ (∃a∈s, a < b),
id               └─┘     └────────────────────────┘                  
src              └─┘       └────────────────────────┘                    
typ              └─┘     └────────────────────────┘                  
doc              └─┘
185      have b ≤ Inf s,
id              └─┘ 
src              └─┘
typ             └─┘ 
doc               └─┘
186        from le_Inf $ assume a ha, le_of_not_gt $ assume h, this ⟨a, ha, h⟩,
id              └────┘           └┘  └──────────┘            └──┘    └┘  
src             └────┘                └──────────┘
typ             └────┘           └┘  └──────────┘            └──┘    └┘  
187      lt_irrefl b (lt_of_le_of_lt ‹b ≤ Inf s› ‹Inf s < b›))
id       └───────┘   └────────────┘   └─┘  └─┘   
src      └───────┘    └────────────┘    └─┘   └─┘     
typ      └───────┘   └────────────┘   └─┘  └─┘   
doc                                      └─┘   └─┘      
188    (assume ⟨a, ha, h⟩, lt_of_le_of_lt (Inf_le ha) h)
id                └┘     └────────────┘  └────┘
src                        └────────────┘  └────┘
typ               └┘     └────────────┘  └────┘
189  
190  lemma lt_Sup_iff : b < Sup s ↔ (∃a∈s, b < a) :=
id                        └─┘        
src                        └─┘           
typ                       └─┘        
doc                         └─┘
191  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
192    (assume : b < Sup s, classical.by_contradiction $ assume : ¬ (∃a∈s, b < a),
id                 └─┘   └────────────────────────┘                  
src                 └─┘    └────────────────────────┘                    
typ                └─┘   └────────────────────────┘                  
doc                  └─┘
193      have Sup s ≤ b,
id            └─┘   
src           └─┘   
typ           └─┘   
doc           └─┘
194        from Sup_le $ assume a ha, le_of_not_gt $ assume h, this ⟨a, ha, h⟩,
id              └────┘           └┘  └──────────┘            └──┘    └┘  
src             └────┘                └──────────┘
typ             └────┘           └┘  └──────────┘            └──┘    └┘  
195      lt_irrefl b (lt_of_lt_of_le ‹b < Sup s› ‹Sup s ≤ b›))
id       └───────┘   └────────────┘   └─┘  └─┘   
src      └───────┘    └────────────┘    └─┘   └─┘     
typ      └───────┘   └────────────┘   └─┘  └─┘   
doc                                      └─┘   └─┘      
196    (assume ⟨a, ha, h⟩, lt_of_lt_of_le h $ le_Sup ha)
id                └┘     └────────────┘     └────┘
src                        └────────────┘     └────┘
typ               └┘     └────────────┘     └────┘
197  
198  lemma Sup_eq_top : Sup s = ⊤ ↔ (∀b<⊤, ∃a∈s, b < a) :=
id                      └─┘              
src                     └─┘                 
typ                     └─┘              
doc                     └─┘
199  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
200    (assume (h : Sup s = ⊤) b hb, by rwa [←h, lt_Sup_iff] at hb)
id                  └─┘      └┘             └────────┘
src                 └─┘               └────┘ └┘└────────┘└─────┘
typ                 └─┘      └┘     └────┘└┘└────────┘└─────┘
doc                 └─┘                 └────┘ └┘          └─────┘
txt                                     └────┘ └┘          └─────┘
par                                     └────┘ └┘          └─────┘
pid                                        └─┘ └┘          └────┘
st                                     └──────┘└──────────┘└────┘
201    (assume h, top_unique $ le_of_not_gt $ assume h',
id               └────────┘   └──────────┘          └┘
src               └────────┘   └──────────┘
typ              └────────┘   └──────────┘          └┘
202      let ⟨a, ha, h⟩ := h _ h' in
id       └─┘    └┘          └┘
typ      └─┘    └┘          └┘
203      lt_irrefl a $ lt_of_le_of_lt (le_Sup ha) h)
id       └───────┘     └────────────┘  └────┘
src      └───────┘     └────────────┘  └────┘
typ      └───────┘     └────────────┘  └────┘
204  
205  lemma Inf_eq_bot : Inf s = ⊥ ↔ (∀b>⊥, ∃a∈s, a < b) :=
id                      └─┘              
src                     └─┘                 
typ                     └─┘              
doc                     └─┘
206  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
207    (assume (h : Inf s = ⊥) b (hb : ⊥ < b), by rwa [←h, Inf_lt_iff] at hb)
id                  └─┘                            └────────┘
src                 └─┘                       └────┘ └┘└────────┘└─────┘
typ                 └─┘                    └────┘└┘└────────┘└─────┘
doc                 └─┘                           └────┘ └┘          └─────┘
txt                                               └────┘ └┘          └─────┘
par                                               └────┘ └┘          └─────┘
pid                                                  └─┘ └┘          └────┘
st                                               └──────┘└──────────┘└────┘
208    (assume h, bot_unique $ le_of_not_gt $ assume h',
id               └────────┘   └──────────┘          └┘
src               └────────┘   └──────────┘
typ              └────────┘   └──────────┘          └┘
209      let ⟨a, ha, h⟩ := h _ h' in
id       └─┘    └┘          └┘
typ      └─┘    └┘          └┘
210      lt_irrefl a $ lt_of_lt_of_le h (Inf_le ha))
id       └───────┘     └────────────┘    └────┘
src      └───────┘     └────────────┘    └────┘
typ      └───────┘     └────────────┘    └────┘
211  
212  lemma lt_supr_iff {ι : Sort*} {f : ι → α} : a < supr f ↔ (∃i, a < f i) :=
id                                               └──┘        
src                                                 └──┘         
typ                                              └──┘        
doc                                                  └──┘
213  iff.trans lt_Sup_iff $ iff.intro
id   └───────┘ └────────┘   └───────┘
src  └───────┘ └────────┘   └───────┘
typ  └───────┘ └────────┘   └───────┘
214    (assume ⟨a', ⟨i, rfl⟩, ha⟩, ⟨i, ha⟩)
id                    └─┘   └┘
src                     └─┘
typ                   └─┘   └┘
215    (assume ⟨i, hi⟩, ⟨f i, ⟨i, rfl⟩, hi⟩)
id               └┘            └─┘
src                               └─┘
typ              └┘            └─┘
216  
217  lemma infi_lt_iff {ι : Sort*} {f : ι → α} : infi f < a ↔ (∃i, f i < a) :=
id                                             └──┘          
src                                              └──┘              
typ                                            └──┘          
doc                                              └──┘
218  iff.trans Inf_lt_iff $ iff.intro
id   └───────┘ └────────┘   └───────┘
src  └───────┘ └────────┘   └───────┘
typ  └───────┘ └────────┘   └───────┘
219    (assume ⟨a', ⟨i, rfl⟩, ha⟩, ⟨i, ha⟩)
id                    └─┘   └┘
src                     └─┘
typ                   └─┘   └┘
220    (assume ⟨i, hi⟩, ⟨f i, ⟨i, rfl⟩, hi⟩)
id               └┘            └─┘
src                               └─┘
typ              └┘            └─┘
221  
222  end complete_linear_order
223  
224  /- supr & infi -/
225  
226  section
227  variables [complete_lattice α] {s t : ι → α} {a b : α}
id              └──────────────┘
src             └──────────────┘
typ             └──────────────┘
doc             └──────────────┘
228  
229  -- TODO: this declaration gives error when starting smt state
230  --@[ematch]
231  theorem le_supr (s : ι → α) (i : ι) : s i ≤ supr s :=
id                                         └──┘ 
src                                             └──┘
typ                                        └──┘ 
doc                                              └──┘
232  le_Sup ⟨i, rfl⟩
id   └────┘    └─┘
src  └────┘     └─┘
typ  └────┘    └─┘
233  
234  @[ematch] theorem le_supr' (s : ι → α) (i : ι) : (: s i ≤ supr s :) :=
id                                                       └──┘ 
src    └────┘                                                 └──┘
typ                                                      └──┘ 
doc    └────┘                                                  └──┘
235  le_Sup ⟨i, rfl⟩
id   └────┘    └─┘
src  └────┘     └─┘
typ  └────┘    └─┘
236  
237  /- TODO: this version would be more powerful, but, alas, the pattern matcher
238     doesn't accept it.
239  @[ematch] theorem le_supr' (s : ι → α) (i : ι) : (: s i :) ≤ (: supr s :) :=
240  le_Sup ⟨i, rfl⟩
241  -/
242  
243  lemma is_lub_supr : is_lub (range s) (⨆j, s j) := is_lub_Sup
id                       └────┘  └───┘           └────────┘
src                      └────┘  └───┘               └────────┘
typ                      └────┘  └───┘           └────────┘
doc                      └────┘  └───┘      
244  
245  lemma is_lub_iff_supr_eq : is_lub (range s) a ↔ (⨆j, s j) = a := is_lub_iff_eq_of_is_lub is_lub_supr
id                              └────┘  └───┘               └─────────────────────┘ └─────────┘
src                             └────┘  └───┘                     └─────────────────────┘ └─────────┘
typ                             └────┘  └───┘               └─────────────────────┘ └─────────┘
doc                             └────┘  └───┘          
246  
247  lemma is_glb_infi : is_glb (range s) (⨅j, s j) := is_glb_Inf
id                       └────┘  └───┘           └────────┘
src                      └────┘  └───┘               └────────┘
typ                      └────┘  └───┘           └────────┘
doc                      └────┘  └───┘      
248  
249  lemma is_glb_iff_infi_eq : is_glb (range s) a ↔ (⨅j, s j) = a := is_glb_iff_eq_of_is_glb is_glb_infi
id                              └────┘  └───┘               └─────────────────────┘ └─────────┘
src                             └────┘  └───┘                     └─────────────────────┘ └─────────┘
typ                             └────┘  └───┘               └─────────────────────┘ └─────────┘
doc                             └────┘  └───┘          
250  
251  theorem le_supr_of_le (i : ι) (h : a ≤ s i) : a ≤ supr s :=
id                                              └──┘ 
src                                                  └──┘
typ                                             └──┘ 
doc                                                    └──┘
252  le_trans h (le_supr _ i)
id   └──────┘   └─────┘   
src  └──────┘    └─────┘
typ  └──────┘   └─────┘   
253  
254  theorem supr_le (h : ∀i, s i ≤ a) : supr s ≤ a :=
id                                  └──┘   
src                                     └──┘   
typ                                 └──┘   
doc                                      └──┘
255  Sup_le $ assume b ⟨i, eq⟩, eq ▸ h i
id   └────┘             └┘       
src  └────┘                └┘      
typ  └────┘             └┘       
256  
257  theorem supr_le_supr (h : ∀i, s i ≤ t i) : supr s ≤ supr t :=
id                                        └──┘   └──┘ 
src                                            └──┘    └──┘
typ                                       └──┘   └──┘ 
doc                                             └──┘     └──┘
258  supr_le $ assume i, le_supr_of_le i (h i)
id   └─────┘            └───────────┘    
src  └─────┘             └───────────┘
typ  └─────┘            └───────────┘    
259  
260  theorem supr_le_supr2 {t : ι₂ → α} (h : ∀i, ∃j, s i ≤ t j) : supr s ≤ supr t :=
id                              └┘                      └──┘   └──┘ 
src                                                            └──┘    └──┘
typ                             └┘                      └──┘   └──┘ 
doc                                                               └──┘     └──┘
261  supr_le $ assume j, exists.elim (h j) le_supr_of_le
id   └─────┘            └─────────┘     └───────────┘
src  └─────┘             └─────────┘       └───────────┘
typ  └─────┘            └─────────┘     └───────────┘
262  
263  theorem supr_le_supr_const (h : ι → ι₂) : (⨆ i:ι, a) ≤ (⨆ j:ι₂, a) :=
id                                      └┘                └┘ 
src                                                            
typ                                     └┘                └┘ 
doc                                                             
264  supr_le $ le_supr _ ∘ h
id   └─────┘   └─────┘    
src  └─────┘   └─────┘   
typ  └─────┘   └─────┘    
265  
266  @[simp] theorem supr_le_iff : supr s ≤ a ↔ (∀i, s i ≤ a) :=
id                                 └──┘            
src                                └──┘                
typ                                └──┘            
doc    └──┘                        └──┘
267  ⟨assume : supr s ≤ a, assume i, le_trans (le_supr _ _) this, supr_le⟩
id             └──┘              └──────┘  └─────┘      └──┘  └─────┘
src            └──┘                 └──────┘  └─────┘            └─────┘
typ            └──┘              └──────┘  └─────┘      └──┘  └─────┘
doc            └──┘
268  
269  -- TODO: finish doesn't do well here.
270  @[congr] theorem supr_congr_Prop {α : Type u} [has_Sup α] {p q : Prop} {f₁ : p → α} {f₂ : q → α}
id                                                  └─────┘                                    
src    └───┘                                        └─────┘
typ                                                 └─────┘                                    
doc    └───┘                                        └─────┘
271    (pq : p ↔ q) (f : ∀x, f₁ (pq.mpr x) = f₂ x) : supr f₁ = supr f₂ :=
id                       └┘  └┘└──┘    └┘     └──┘ └┘  └──┘ └┘
src                               └──┘             └──┘     └──┘
typ                      └┘  └┘└──┘    └┘     └──┘ └┘  └──┘ └┘
doc                                                  └──┘      └──┘
272  begin
st   └─────
273    unfold supr,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
274    apply congr_arg,
id           └───────┘
src    └────┘└───────┘
typ    └────┘└───────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────────────┘└─
275    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
276    simp,
src    └──┘
typ    └──┘
doc    └──┘
txt    └──┘
par    └──┘
st   ─────┘└─
277    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
278    exact λ⟨h, W⟩, ⟨pq.1 h, eq.trans (f (pq.1 h)).symm W⟩,
id                           └──────┘    └┘
src    └────┘  └┘ └─┘   └─┘ └┘└──────┘     └─┘ └──────┘ 
typ    └────┘ └┘└─┘   └─┘ └┘└──────┘  └┘└─┘ └──────┘ 
doc    └────┘  └┘ └─┘   └─┘ └┘             └─┘ └──────┘ 
txt    └────┘  └┘ └─┘   └─┘ └┘             └─┘ └──────┘ 
par    └────┘  └┘ └─┘   └─┘ └┘             └─┘ └──────┘ 
pid           └┘ └─┘   └─┘ └┘             └─┘ └──────┘ 
st   ──────────────────────────────────────────────────────┘└─
279    exact λ⟨h, W⟩, ⟨pq.2 h, eq.trans (f h) W⟩
id                   └┘      └──────┘  
src    └────┘  └┘ └─┘   └─┘ └┘└──────┘   └┘ └┘
typ    └────┘ └┘└─┘ └┘└─┘ └┘└──────┘  └┘ └┘
doc    └────┘  └┘ └─┘   └─┘ └┘           └┘ └┘
txt    └────┘  └┘ └─┘   └─┘ └┘           └┘ └┘
par    └────┘  └┘ └─┘   └─┘ └┘           └┘ └┘
pid           └┘ └─┘   └─┘ └┘           └┘ 
st   ───────────────────────────────────────────┘
280  end
st   └─┘
281  
282  theorem infi_le (s : ι → α) (i : ι) : infi s ≤ s i :=
id                                      └──┘    
src                                        └──┘   
typ                                     └──┘    
doc                                        └──┘
283  Inf_le ⟨i, rfl⟩
id   └────┘    └─┘
src  └────┘     └─┘
typ  └────┘    └─┘
284  
285  @[ematch] theorem infi_le' (s : ι → α) (i : ι) : (: infi s ≤ s i :) :=
id                                                    └──┘    
src    └────┘                                            └──┘   
typ                                                   └──┘    
doc    └────┘                                            └──┘
286  Inf_le ⟨i, rfl⟩
id   └────┘    └─┘
src  └────┘     └─┘
typ  └────┘    └─┘
287  
288  /- I wanted to see if this would help for infi_comm; it doesn't.
289  @[ematch] theorem infi_le₂' (s : ι → ι₂ → α) (i : ι) (j : ι₂) : (: ⨅ i j, s i j :) ≤ (: s i j :) :=
290  begin
291    transitivity,
292    apply (infi_le (λ i, ⨅ j, s i j) i),
293    apply infi_le
294  end
295  -/
296  
297  theorem infi_le_of_le (i : ι) (h : s i ≤ a) : infi s ≤ a :=
id                                            └──┘   
src                                               └──┘   
typ                                           └──┘   
doc                                                └──┘
298  le_trans (infi_le _ i) h
id   └──────┘  └─────┘     
src  └──────┘  └─────┘
typ  └──────┘  └─────┘     
299  
300  theorem le_infi (h : ∀i, a ≤ s i) : a ≤ infi s :=
id                                    └──┘ 
src                                        └──┘
typ                                   └──┘ 
doc                                          └──┘
301  le_Inf $ assume b ⟨i, eq⟩, eq ▸ h i
id   └────┘             └┘       
src  └────┘                └┘      
typ  └────┘             └┘       
302  
303  theorem infi_le_infi (h : ∀i, s i ≤ t i) : infi s ≤ infi t :=
id                                        └──┘   └──┘ 
src                                            └──┘    └──┘
typ                                       └──┘   └──┘ 
doc                                             └──┘     └──┘
304  le_infi $ assume i, infi_le_of_le i (h i)
id   └─────┘            └───────────┘    
src  └─────┘             └───────────┘
typ  └─────┘            └───────────┘    
305  
306  theorem infi_le_infi2 {t : ι₂ → α} (h : ∀j, ∃i, s i ≤ t j) : infi s ≤ infi t :=
id                              └┘                      └──┘   └──┘ 
src                                                            └──┘    └──┘
typ                             └┘                      └──┘   └──┘ 
doc                                                               └──┘     └──┘
307  le_infi $ assume j, exists.elim (h j) infi_le_of_le
id   └─────┘            └─────────┘     └───────────┘
src  └─────┘             └─────────┘       └───────────┘
typ  └─────┘            └─────────┘     └───────────┘
308  
309  theorem infi_le_infi_const (h : ι₂ → ι) : (⨅ i:ι, a) ≤ (⨅ j:ι₂, a) :=
id                                   └┘                   └┘ 
src                                                            
typ                                  └┘                   └┘ 
doc                                                             
310  le_infi $ infi_le _ ∘ h
id   └─────┘   └─────┘    
src  └─────┘   └─────┘   
typ  └─────┘   └─────┘    
311  
312  @[simp] theorem le_infi_iff : a ≤ infi s ↔ (∀i, a ≤ s i) :=
id                                   └──┘          
src                                   └──┘           
typ                                  └──┘          
doc    └──┘                            └──┘
313  ⟨assume : a ≤ infi s, assume i, le_trans this (infi_le _ _), le_infi⟩
id               └──┘            └──────┘ └──┘  └─────┘       └─────┘
src               └──┘              └──────┘       └─────┘       └─────┘
typ              └──┘            └──────┘ └──┘  └─────┘       └─────┘
doc                └──┘
314  
315  @[congr] theorem infi_congr_Prop {α : Type u} [has_Inf α] {p q : Prop} {f₁ : p → α} {f₂ : q → α}
id                                                  └─────┘                                    
src    └───┘                                        └─────┘
typ                                                 └─────┘                                    
doc    └───┘                                        └─────┘
316    (pq : p ↔ q) (f : ∀x, f₁ (pq.mpr x) = f₂ x) : infi f₁ = infi f₂ :=
id                       └┘  └┘└──┘    └┘     └──┘ └┘  └──┘ └┘
src                               └──┘             └──┘     └──┘
typ                      └┘  └┘└──┘    └┘     └──┘ └┘  └──┘ └┘
doc                                                  └──┘      └──┘
317  begin
st   └─────
318    unfold infi,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
319    apply congr_arg,
id           └───────┘
src    └────┘└───────┘
typ    └────┘└───────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────────────┘└─
320    ext,
src    └─┘
typ    └─┘
doc    └─┘
txt    └─┘
par    └─┘
st   ────┘└─
321    simp,
src    └──┘
typ    └──┘
doc    └──┘
txt    └──┘
par    └──┘
st   ─────┘└─
322    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
323    exact λ⟨h, W⟩, ⟨pq.1 h, eq.trans (f (pq.1 h)).symm W⟩,
id                           └──────┘    └┘
src    └────┘  └┘ └─┘   └─┘ └┘└──────┘     └─┘ └──────┘ 
typ    └────┘ └┘└─┘   └─┘ └┘└──────┘  └┘└─┘ └──────┘ 
doc    └────┘  └┘ └─┘   └─┘ └┘             └─┘ └──────┘ 
txt    └────┘  └┘ └─┘   └─┘ └┘             └─┘ └──────┘ 
par    └────┘  └┘ └─┘   └─┘ └┘             └─┘ └──────┘ 
pid           └┘ └─┘   └─┘ └┘             └─┘ └──────┘ 
st   ──────────────────────────────────────────────────────┘└─
324    exact λ⟨h, W⟩, ⟨pq.2 h, eq.trans (f h) W⟩
id                   └┘      └──────┘  
src    └────┘  └┘ └─┘   └─┘ └┘└──────┘   └┘ └┘
typ    └────┘ └┘└─┘ └┘└─┘ └┘└──────┘  └┘ └┘
doc    └────┘  └┘ └─┘   └─┘ └┘           └┘ └┘
txt    └────┘  └┘ └─┘   └─┘ └┘           └┘ └┘
par    └────┘  └┘ └─┘   └─┘ └┘           └┘ └┘
pid           └┘ └─┘   └─┘ └┘           └┘ 
st   ───────────────────────────────────────────┘
325  end
st   └─┘
326  
327  @[simp] theorem infi_const {a : α} : ∀[nonempty ι], (⨅ b:ι, a) = a
id                                        └──────┘            
src                                         └──────┘              
typ                                       └──────┘            
doc    └──┘                                                   
328  | ⟨i⟩ := le_antisymm (Inf_le ⟨i, rfl⟩) (by finish)
id           └─────────┘  └────┘     └─┘
src           └─────────┘  └────┘     └─┘       └────┘
typ          └─────────┘  └────┘     └─┘       └────┘
doc                                             └────┘
txt                                             └────┘
par                                             └────┘
st                                             └─────┘
329  
330  @[simp] theorem supr_const {a : α} : ∀[nonempty ι], (⨆ b:ι, a) = a
id                                        └──────┘            
src                                         └──────┘              
typ                                       └──────┘            
doc    └──┘                                                   
331  | ⟨i⟩ := le_antisymm (by finish) (le_Sup ⟨i, rfl⟩)
id           └─────────┘              └────┘     └─┘
src           └─────────┘     └────┘   └────┘     └─┘
typ          └─────────┘     └────┘   └────┘     └─┘
doc                           └────┘
txt                           └────┘
par                           └────┘
st                           └─────┘
332  
333  @[simp] lemma infi_top : (⨅i:ι, ⊤ : α) = ⊤ :=
id                                      
src                                       
typ                                     
doc    └──┘                       
334  top_unique $ le_infi $ assume i, le_refl _
id   └────────┘   └─────┘            └─────┘
src  └────────┘   └─────┘             └─────┘
typ  └────────┘   └─────┘            └─────┘
335  
336  @[simp] lemma supr_bot : (⨆i:ι, ⊥ : α) = ⊥ :=
id                                      
src                                       
typ                                     
doc    └──┘                       
337  bot_unique $ supr_le $ assume i, le_refl _
id   └────────┘   └─────┘            └─────┘
src  └────────┘   └─────┘             └─────┘
typ  └────────┘   └─────┘            └─────┘
338  
339  @[simp] lemma infi_eq_top : infi s = ⊤ ↔ (∀i, s i = ⊤) :=
id                               └──┘            
src                              └──┘                
typ                              └──┘            
doc    └──┘                      └──┘
340  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
341    (assume eq i, top_unique $ eq ▸ infi_le _ _)
id             └┘   └────────┘   └┘  └─────┘
src            └┘    └────────┘   └┘  └─────┘
typ            └┘   └────────┘   └┘  └─────┘
342    (assume h, top_unique $ le_infi $ assume i, top_le_iff.2 $ h i)
id               └────────┘   └─────┘            └────────┘     
src               └────────┘   └─────┘             └────────┘
typ              └────────┘   └─────┘            └────────┘     
343  
344  @[simp] lemma supr_eq_bot : supr s = ⊥ ↔ (∀i, s i = ⊥) :=
id                               └──┘            
src                              └──┘                
typ                              └──┘            
doc    └──┘                      └──┘
345  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
346    (assume eq i, bot_unique $ eq ▸ le_supr _ _)
id             └┘   └────────┘   └┘  └─────┘
src            └┘    └────────┘   └┘  └─────┘
typ            └┘   └────────┘   └┘  └─────┘
347    (assume h, bot_unique $ supr_le $ assume i, le_bot_iff.2 $ h i)
id               └────────┘   └─────┘            └────────┘     
src               └────────┘   └─────┘             └────────┘
typ              └────────┘   └─────┘            └────────┘     
348  
349  @[simp] lemma infi_pos {p : Prop} {f : p → α} (hp : p) : (⨅ h : p, f h) = f hp :=
id                                                                     └┘
src                                                                        
typ                                                                    └┘
doc    └──┘                                                          
350  le_antisymm (infi_le _ _) (le_infi $ assume h, le_refl _)
id   └─────────┘  └─────┘       └─────┘            └─────┘
src  └─────────┘  └─────┘       └─────┘             └─────┘
typ  └─────────┘  └─────┘       └─────┘            └─────┘
351  
352  @[simp] lemma infi_neg {p : Prop} {f : p → α} (hp : ¬ p) : (⨅ h : p, f h) = ⊤ :=
id                                                                     
src                                                                          
typ                                                                    
doc    └──┘                                                            
353  le_antisymm le_top $ le_infi $ assume h, (hp h).elim
id   └─────────┘ └────┘   └─────┘             └┘  └──┘
src  └─────────┘ └────┘   └─────┘                   └──┘
typ  └─────────┘ └────┘   └─────┘             └┘  └──┘
354  
355  @[simp] lemma supr_pos {p : Prop} {f : p → α} (hp : p) : (⨆ h : p, f h) = f hp :=
id                                                                     └┘
src                                                                        
typ                                                                    └┘
doc    └──┘                                                          
356  le_antisymm (supr_le $ assume h, le_refl _) (le_supr _ _)
id   └─────────┘  └─────┘            └─────┘     └─────┘
src  └─────────┘  └─────┘             └─────┘     └─────┘
typ  └─────────┘  └─────┘            └─────┘     └─────┘
357  
358  @[simp] lemma supr_neg {p : Prop} {f : p → α} (hp : ¬ p) : (⨆ h : p, f h) = ⊥ :=
id                                                                     
src                                                                          
typ                                                                    
doc    └──┘                                                            
359  le_antisymm (supr_le $ assume h, (hp h).elim) bot_le
id   └─────────┘  └─────┘             └┘  └──┘   └────┘
src  └─────────┘  └─────┘                   └──┘   └────┘
typ  └─────────┘  └─────┘             └┘  └──┘   └────┘
360  
361  lemma supr_eq_dif {p : Prop} [decidable p] (a : p → α) :
id                                 └───────┘           
src                                └───────┘
typ                                └───────┘           
362    (⨆h:p, a h) = (if h : p then a h else ⊥) :=
id              └┘                  
src                └┘                     
typ             └┘                  
doc        
363  by by_cases p; simp [h]
id                       
src     └───────┘   └────┘ └─
typ     └───────┘  └────┘└─
doc     └───────┘   └────┘ └─
txt     └───────┘   └────┘ └─
par     └───────┘   └────┘ └─
pid                     
st     └─────────────────────
364  
src  
typ  
doc  
txt  
par  
pid  
st   
365  lemma supr_eq_if {p : Prop} [decidable p] (a : α) :
id                                └───────┘        
src                               └───────┘
typ                               └───────┘        
366    (⨆h:p, a) = (if p then a else ⊥) :=
id                            
src                               
typ                           
doc        
367  by rw [supr_eq_dif, dif_eq_if]
id          └─────────┘  └───────┘
src     └──┘└─────────┘└┘└───────┘└─
typ     └──┘└─────────┘└┘└───────┘└─
doc     └──┘           └┘         └─
txt     └──┘           └┘         └─
par     └──┘           └┘         └─
pid       └┘           └┘         
st     └──────────────┘└─────────┘
368  
src  
typ  
doc  
txt  
par  
pid  
st   
369  lemma infi_eq_dif {p : Prop} [decidable p] (a : p → α) :
id                                 └───────┘           
src                                └───────┘
typ                                └───────┘           
370    (⨅h:p, a h) = (if h : p then a h else ⊤) :=
id              └┘                  
src                └┘                     
typ             └┘                  
doc        
371  by by_cases p; simp [h]
id                       
src     └───────┘   └────┘ └─
typ     └───────┘  └────┘└─
doc     └───────┘   └────┘ └─
txt     └───────┘   └────┘ └─
par     └───────┘   └────┘ └─
pid                     
st     └─────────────────────
372  
src  
typ  
doc  
txt  
par  
pid  
st   
373  lemma infi_eq_if {p : Prop} [decidable p] (a : α) :
id                                └───────┘        
src                               └───────┘
typ                               └───────┘        
374    (⨅h:p, a) = (if p then a else ⊤) :=
id                            
src                               
typ                           
doc        
375  by rw [infi_eq_dif, dif_eq_if]
id          └─────────┘  └───────┘
src     └──┘└─────────┘└┘└───────┘└─
typ     └──┘└─────────┘└┘└───────┘└─
doc     └──┘           └┘         └─
txt     └──┘           └┘         └─
par     └──┘           └┘         └─
pid       └┘           └┘         
st     └──────────────┘└─────────┘
376  
src  
typ  
doc  
txt  
par  
pid  
st   
377  -- TODO: should this be @[simp]?
src  ────────────────────────────────┘
typ  ────────────────────────────────┘
doc  ────────────────────────────────┘
txt  ────────────────────────────────┘
par  ────────────────────────────────┘
pid  ────────────────────────────────┘
st   ────────────────────────────────┘
378  theorem infi_comm {f : ι → ι₂ → α} : (⨅i, ⨅j, f i j) = (⨅j, ⨅i, f i j) :=
id                             └┘                    
src                                                        
typ                            └┘                    
doc                                                         
379  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
380    (le_infi $ assume i, le_infi $ assume j, infi_le_of_le j $ infi_le _ i)
id      └─────┘            └─────┘            └───────────┘    └─────┘   
src     └─────┘             └─────┘             └───────────┘     └─────┘
typ     └─────┘            └─────┘            └───────────┘    └─────┘   
381    (le_infi $ assume j, le_infi $ assume i, infi_le_of_le i $ infi_le _ j)
id      └─────┘            └─────┘            └───────────┘    └─────┘   
src     └─────┘             └─────┘             └───────────┘     └─────┘
typ     └─────┘            └─────┘            └───────────┘    └─────┘   
382  
383  /- TODO: this is strange. In the proof below, we get exactly the desired
384     among the equalities, but close does not get it.
385  begin
386    apply @le_antisymm,
387      simp, intros,
388      begin [smt]
389        ematch, ematch, ematch, trace_state, have := le_refl (f i_1 i),
390        trace_state, close
391      end
392  end
393  -/
394  
395  -- TODO: should this be @[simp]?
396  theorem supr_comm {f : ι → ι₂ → α} : (⨆i, ⨆j, f i j) = (⨆j, ⨆i, f i j) :=
id                             └┘                    
src                                                        
typ                            └┘                    
doc                                                         
397  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
398    (supr_le $ assume i, supr_le $ assume j, le_supr_of_le j $ le_supr _ i)
id      └─────┘            └─────┘            └───────────┘    └─────┘   
src     └─────┘             └─────┘             └───────────┘     └─────┘
typ     └─────┘            └─────┘            └───────────┘    └─────┘   
399    (supr_le $ assume j, supr_le $ assume i, le_supr_of_le i $ le_supr _ j)
id      └─────┘            └─────┘            └───────────┘    └─────┘   
src     └─────┘             └─────┘             └───────────┘     └─────┘
typ     └─────┘            └─────┘            └───────────┘    └─────┘   
400  
401  @[simp] theorem infi_infi_eq_left {b : β} {f : Πx:β, x = b → α} : (⨅x, ⨅h:x = b, f x h) = f b rfl :=
id                                                                             └─┘
src                                                                                         └─┘
typ                                                                            └─┘
doc    └──┘                                                                      
402  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
403    (infi_le_of_le b $ infi_le _ rfl)
id      └───────────┘    └─────┘   └─┘
src     └───────────┘     └─────┘   └─┘
typ     └───────────┘    └─────┘   └─┘
404    (le_infi $ assume b', le_infi $ assume eq, match b', eq with ._, rfl := le_refl _ end)
id      └─────┘          └┘  └─────┘          └┘        └┘  └┘          └─┘    └─────┘
src     └─────┘              └─────┘          └┘            └┘          └─┘    └─────┘
typ     └─────┘          └┘  └─────┘          └┘        └┘  └┘          └─┘    └─────┘
405  
406  @[simp] theorem infi_infi_eq_right {b : β} {f : Πx:β, b = x → α} : (⨅x, ⨅h:b = x, f x h) = f b rfl :=
id                                                                              └─┘
src                                                                                          └─┘
typ                                                                             └─┘
doc    └──┘                                                                       
407  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
408    (infi_le_of_le b $ infi_le _ rfl)
id      └───────────┘    └─────┘   └─┘
src     └───────────┘     └─────┘   └─┘
typ     └───────────┘    └─────┘   └─┘
409    (le_infi $ assume b', le_infi $ assume eq, match b', eq with ._, rfl := le_refl _ end)
id      └─────┘          └┘  └─────┘          └┘        └┘  └┘          └─┘    └─────┘
src     └─────┘              └─────┘          └┘            └┘          └─┘    └─────┘
typ     └─────┘          └┘  └─────┘          └┘        └┘  └┘          └─┘    └─────┘
410  
411  @[simp] theorem supr_supr_eq_left {b : β} {f : Πx:β, x = b → α} : (⨆x, ⨆h : x = b, f x h) = f b rfl :=
id                                                                               └─┘
src                                                                                           └─┘
typ                                                                              └─┘
doc    └──┘                                                                        
412  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
413    (supr_le $ assume b', supr_le $ assume eq, match b', eq with ._, rfl := le_refl _ end)
id      └─────┘          └┘  └─────┘          └┘        └┘  └┘          └─┘    └─────┘
src     └─────┘              └─────┘          └┘            └┘          └─┘    └─────┘
typ     └─────┘          └┘  └─────┘          └┘        └┘  └┘          └─┘    └─────┘
414    (le_supr_of_le b $ le_supr _ rfl)
id      └───────────┘    └─────┘   └─┘
src     └───────────┘     └─────┘   └─┘
typ     └───────────┘    └─────┘   └─┘
415  
416  @[simp] theorem supr_supr_eq_right {b : β} {f : Πx:β, b = x → α} : (⨆x, ⨆h : b = x, f x h) = f b rfl :=
id                                                                                └─┘
src                                                                                            └─┘
typ                                                                               └─┘
doc    └──┘                                                                         
417  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
418    (supr_le $ assume b', supr_le $ assume eq, match b', eq with ._, rfl := le_refl _ end)
id      └─────┘          └┘  └─────┘          └┘        └┘  └┘          └─┘    └─────┘
src     └─────┘              └─────┘          └┘            └┘          └─┘    └─────┘
typ     └─────┘          └┘  └─────┘          └┘        └┘  └┘          └─┘    └─────┘
419    (le_supr_of_le b $ le_supr _ rfl)
id      └───────────┘    └─────┘   └─┘
src     └───────────┘     └─────┘   └─┘
typ     └───────────┘    └─────┘   └─┘
420  
421  attribute [ematch] le_refl
id                      └─────┘
src             └────┘  └─────┘
typ                     └─────┘
doc             └────┘
422  
423  theorem infi_inf_eq {f g : ι → α} : (⨅ x, f x ⊓ g x) = (⨅ x, f x) ⊓ (⨅ x, g x) :=
id                                                          
src                                                                  
typ                                                         
doc                                                                     
424  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
425    (le_inf
id      └────┘
src     └────┘
typ     └────┘
426      (le_infi $ assume i, infi_le_of_le i inf_le_left)
id        └─────┘            └───────────┘  └─────────┘
src       └─────┘             └───────────┘   └─────────┘
typ       └─────┘            └───────────┘  └─────────┘
427      (le_infi $ assume i, infi_le_of_le i inf_le_right))
id        └─────┘            └───────────┘  └──────────┘
src       └─────┘             └───────────┘   └──────────┘
typ       └─────┘            └───────────┘  └──────────┘
428    (le_infi $ assume i, le_inf
id      └─────┘            └────┘
src     └─────┘             └────┘
typ     └─────┘            └────┘
429      (inf_le_left_of_le $ infi_le _ _)
id        └───────────────┘   └─────┘
src       └───────────────┘   └─────┘
typ       └───────────────┘   └─────┘
430      (inf_le_right_of_le $ infi_le _ _))
id        └────────────────┘   └─────┘
src       └────────────────┘   └─────┘
typ       └────────────────┘   └─────┘
431  
432  /- TODO: here is another example where more flexible pattern matching
433     might help.
434  
435  begin
436    apply @le_antisymm,
437    safe, pose h := f a ⊓ g a, begin [smt] ematch, ematch  end
438  end
439  -/
440  
441  lemma infi_inf {f : ι → α} {a : α} (i : ι) : (⨅x, f x) ⊓ a = (⨅ x, f x ⊓ a) :=
id                                                          
src                                                                   
typ                                                         
doc                                                                
442  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
443    (le_infi $ assume i, le_inf (inf_le_left_of_le $ infi_le _ _) inf_le_right)
id      └─────┘            └────┘  └───────────────┘   └─────┘      └──────────┘
src     └─────┘             └────┘  └───────────────┘   └─────┘      └──────────┘
typ     └─────┘            └────┘  └───────────────┘   └─────┘      └──────────┘
444    (le_inf (infi_le_infi $ assume i, inf_le_left) (infi_le_of_le i inf_le_right))
id      └────┘  └──────────┘            └─────────┘   └───────────┘  └──────────┘
src     └────┘  └──────────┘             └─────────┘   └───────────┘   └──────────┘
typ     └────┘  └──────────┘            └─────────┘   └───────────┘  └──────────┘
445  
446  lemma inf_infi {f : ι → α} {a : α} (i : ι) : a ⊓ (⨅x, f x) = (⨅ x, a ⊓ f x) :=
id                                                          
src                                                                 
typ                                                         
doc                                                                
447  by rw [inf_comm, infi_inf i]; simp [inf_comm]
id          └──────┘  └──────┘          └──────┘
src     └──┘└──────┘└┘└──────┘   └────┘└──────┘└─
typ     └──┘└──────┘└┘└──────┘  └────┘└──────┘└─
doc     └──┘        └┘           └────┘        └─
txt     └──┘        └┘           └────┘        └─
par     └──┘        └┘           └────┘        └─
pid       └┘        └┘                       
st     └───────────┘└──────────┘└─────────────────
448  
src  
typ  
doc  
txt  
par  
pid  
st   
449  lemma binfi_inf {ι : Sort*} {p : ι → Prop}
id                                    
typ                                   
450    {f : Πi, p i → α} {a : α} {i : ι} (hi : p i) :
id                                        
typ                                       
451    (⨅i (h : p i), f i h) ⊓ a = (⨅ i (h : p i), f i h ⊓ a) :=
id                                     
src                                                
typ                                    
doc                                           
452  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
453    (le_infi $ assume i, le_infi $ assume hi,
id      └─────┘            └─────┘          └┘
src     └─────┘             └─────┘
typ     └─────┘            └─────┘          └┘
454      le_inf (inf_le_left_of_le $ infi_le_of_le i $ infi_le _ _) inf_le_right)
id       └────┘  └───────────────┘   └───────────┘    └─────┘      └──────────┘
src      └────┘  └───────────────┘   └───────────┘     └─────┘      └──────────┘
typ      └────┘  └───────────────┘   └───────────┘    └─────┘      └──────────┘
455    (le_inf (infi_le_infi $ assume i, infi_le_infi $ assume hi, inf_le_left)
id      └────┘  └──────────┘            └──────────┘          └┘  └─────────┘
src     └────┘  └──────────┘             └──────────┘              └─────────┘
typ     └────┘  └──────────┘            └──────────┘          └┘  └─────────┘
456       (infi_le_of_le i $ infi_le_of_le hi $ inf_le_right))
id         └───────────┘    └───────────┘ └┘   └──────────┘
src        └───────────┘     └───────────┘      └──────────┘
typ        └───────────┘    └───────────┘ └┘   └──────────┘
457  
458  theorem supr_sup_eq {f g : β → α} : (⨆ x, f x ⊔ g x) = (⨆ x, f x) ⊔ (⨆ x, g x) :=
id                                                          
src                                                                  
typ                                                         
doc                                                                     
459  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
460    (supr_le $ assume i, sup_le
id      └─────┘            └────┘
src     └─────┘             └────┘
typ     └─────┘            └────┘
461      (le_sup_left_of_le $ le_supr _ _)
id        └───────────────┘   └─────┘
src       └───────────────┘   └─────┘
typ       └───────────────┘   └─────┘
462      (le_sup_right_of_le $ le_supr _ _))
id        └────────────────┘   └─────┘
src       └────────────────┘   └─────┘
typ       └────────────────┘   └─────┘
463    (sup_le
id      └────┘
src     └────┘
typ     └────┘
464      (supr_le $ assume i, le_supr_of_le i le_sup_left)
id        └─────┘            └───────────┘  └─────────┘
src       └─────┘             └───────────┘   └─────────┘
typ       └─────┘            └───────────┘  └─────────┘
465      (supr_le $ assume i, le_supr_of_le i le_sup_right))
id        └─────┘            └───────────┘  └──────────┘
src       └─────┘             └───────────┘   └──────────┘
typ       └─────┘            └───────────┘  └──────────┘
466  
467  /- supr and infi under Prop -/
468  
469  @[simp] theorem infi_false {s : false → α} : infi s = ⊤ :=
id                                   └───┘       └──┘   
src                                  └───┘        └──┘    
typ                                  └───┘       └──┘   
doc    └──┘                                       └──┘
470  le_antisymm le_top (le_infi $ assume i, false.elim i)
id   └─────────┘ └────┘  └─────┘            └────────┘ 
src  └─────────┘ └────┘  └─────┘             └────────┘
typ  └─────────┘ └────┘  └─────┘            └────────┘ 
471  
472  @[simp] theorem supr_false {s : false → α} : supr s = ⊥ :=
id                                   └───┘       └──┘   
src                                  └───┘        └──┘    
typ                                  └───┘       └──┘   
doc    └──┘                                       └──┘
473  le_antisymm (supr_le $ assume i, false.elim i) bot_le
id   └─────────┘  └─────┘            └────────┘   └────┘
src  └─────────┘  └─────┘             └────────┘    └────┘
typ  └─────────┘  └─────┘            └────────┘   └────┘
474  
475  @[simp] theorem infi_true {s : true → α} : infi s = s trivial :=
id                                  └──┘       └──┘    └─────┘
src                                 └──┘        └──┘      └─────┘
typ                                 └──┘       └──┘    └─────┘
doc    └──┘                                     └──┘
476  le_antisymm (infi_le _ _) (le_infi $ assume ⟨⟩, le_refl _)
id   └─────────┘  └─────┘       └─────┘             └─────┘
src  └─────────┘  └─────┘       └─────┘             └─────┘
typ  └─────────┘  └─────┘       └─────┘             └─────┘
477  
478  @[simp] theorem supr_true {s : true → α} : supr s = s trivial :=
id                                  └──┘       └──┘    └─────┘
src                                 └──┘        └──┘      └─────┘
typ                                 └──┘       └──┘    └─────┘
doc    └──┘                                     └──┘
479  le_antisymm (supr_le $ assume ⟨⟩, le_refl _) (le_supr _ _)
id   └─────────┘  └─────┘             └─────┘     └─────┘
src  └─────────┘  └─────┘             └─────┘     └─────┘
typ  └─────────┘  └─────┘             └─────┘     └─────┘
480  
481  @[simp] theorem infi_exists {p : ι → Prop} {f : Exists p → α} : (⨅ x, f x) = (⨅ i, ⨅ h:p i, f ⟨i, h⟩) :=
id                                                  └────┘                           
src                                                  └────┘                              
typ                                                 └────┘                           
doc    └──┘                                                                               
482  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
483    (le_infi $ assume i, le_infi $ assume : p i, infi_le _ _)
id      └─────┘            └─────┘               └─────┘
src     └─────┘             └─────┘                 └─────┘
typ     └─────┘            └─────┘               └─────┘
484    (le_infi $ assume ⟨i, h⟩, infi_le_of_le i $ infi_le _ _)
id      └─────┘                └───────────┘     └─────┘
src     └─────┘                  └───────────┘     └─────┘
typ     └─────┘                └───────────┘     └─────┘
485  
486  @[simp] theorem supr_exists {p : ι → Prop} {f : Exists p → α} : (⨆ x, f x) = (⨆ i, ⨆ h:p i, f ⟨i, h⟩) :=
id                                                  └────┘                           
src                                                  └────┘                              
typ                                                 └────┘                           
doc    └──┘                                                                               
487  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
488    (supr_le $ assume ⟨i, h⟩, le_supr_of_le i $ le_supr (λh:p i, f ⟨i, h⟩) _)
id      └─────┘                └───────────┘     └─────┘              
src     └─────┘                  └───────────┘     └─────┘
typ     └─────┘                └───────────┘     └─────┘              
489    (supr_le $ assume i, supr_le $ assume : p i, le_supr _ _)
id      └─────┘            └─────┘               └─────┘
src     └─────┘             └─────┘                 └─────┘
typ     └─────┘            └─────┘               └─────┘
490  
491  theorem infi_and {p q : Prop} {s : p ∧ q → α} : infi s = (⨅ h₁ h₂, s ⟨h₁, h₂⟩) :=
id                                               └──┘     └┘ └┘   └┘  └┘
src                                                 └──┘           
typ                                              └──┘     └┘ └┘   └┘  └┘
doc                                                  └──┘            
492  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
493    (le_infi $ assume i, le_infi $ assume j, infi_le _ _)
id      └─────┘            └─────┘            └─────┘
src     └─────┘             └─────┘             └─────┘
typ     └─────┘            └─────┘            └─────┘
494    (le_infi $ assume ⟨i, h⟩, infi_le_of_le i $ infi_le _ _)
id      └─────┘                └───────────┘     └─────┘
src     └─────┘                  └───────────┘     └─────┘
typ     └─────┘                └───────────┘     └─────┘
495  
496  theorem supr_and {p q : Prop} {s : p ∧ q → α} : supr s = (⨆ h₁ h₂, s ⟨h₁, h₂⟩) :=
id                                               └──┘     └┘ └┘   └┘  └┘
src                                                 └──┘           
typ                                              └──┘     └┘ └┘   └┘  └┘
doc                                                  └──┘            
497  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
498    (supr_le $ assume ⟨i, h⟩, le_supr_of_le i $ le_supr (λj, s ⟨i, j⟩) _)
id      └─────┘                └───────────┘     └─────┘          
src     └─────┘                  └───────────┘     └─────┘
typ     └─────┘                └───────────┘     └─────┘          
499    (supr_le $ assume i, supr_le $ assume j, le_supr _ _)
id      └─────┘            └─────┘            └─────┘
src     └─────┘             └─────┘             └─────┘
typ     └─────┘            └─────┘            └─────┘
500  
501  theorem infi_or {p q : Prop} {s : p ∨ q → α} :
id                                          
src                                      
typ                                         
502    infi s = (⨅ h : p, s (or.inl h)) ⊓ (⨅ h : q, s (or.inr h)) :=
id     └──┘            └────┘              └────┘ 
src    └──┘               └────┘                 └────┘
typ    └──┘            └────┘              └────┘ 
doc    └──┘                                    
503  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
504    (le_inf
id      └────┘
src     └────┘
typ     └────┘
505      (infi_le_infi2 $ assume j, ⟨_, le_refl _⟩)
id        └───────────┘                └─────┘
src       └───────────┘                 └─────┘
typ       └───────────┘                └─────┘
506      (infi_le_infi2 $ assume j, ⟨_, le_refl _⟩))
id        └───────────┘                └─────┘
src       └───────────┘                 └─────┘
typ       └───────────┘                └─────┘
507    (le_infi $ assume i, match i with
id      └─────┘                  
src     └─────┘
typ     └─────┘                  
508    | or.inl i := inf_le_left_of_le $ infi_le _ _
id       └────┘      └───────────────┘   └─────┘
src      └────┘      └───────────────┘   └─────┘
typ      └────┘      └───────────────┘   └─────┘
509    | or.inr j := inf_le_right_of_le $ infi_le _ _
id       └────┘      └────────────────┘   └─────┘
src      └────┘      └────────────────┘   └─────┘
typ      └────┘      └────────────────┘   └─────┘
510    end)
511  
512  theorem supr_or {p q : Prop} {s : p ∨ q → α} :
id                                          
src                                      
typ                                         
513    (⨆ x, s x) = (⨆ i, s (or.inl i)) ⊔ (⨆ j, s (or.inr j)) :=
id                 └────┘          └────┘ 
src                     └────┘             └────┘
typ                └────┘          └────┘ 
doc                                      
514  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
515    (supr_le $ assume s, match s with
id      └─────┘                  
src     └─────┘
typ     └─────┘                  
516    | or.inl i := le_sup_left_of_le $ le_supr _ i
id       └────┘     └───────────────┘   └─────┘
src      └────┘      └───────────────┘   └─────┘
typ      └────┘     └───────────────┘   └─────┘
517    | or.inr j := le_sup_right_of_le $ le_supr _ j
id       └────┘     └────────────────┘   └─────┘
src      └────┘      └────────────────┘   └─────┘
typ      └────┘     └────────────────┘   └─────┘
518    end)
519    (sup_le
id      └────┘
src     └────┘
typ     └────┘
520      (supr_le_supr2 $ assume i, ⟨or.inl i, le_refl _⟩)
id        └───────────┘             └────┘   └─────┘
src       └───────────┘              └────┘    └─────┘
typ       └───────────┘             └────┘   └─────┘
521      (supr_le_supr2 $ assume j, ⟨or.inr j, le_refl _⟩))
id        └───────────┘             └────┘   └─────┘
src       └───────────┘              └────┘    └─────┘
typ       └───────────┘             └────┘   └─────┘
522  
523  theorem Inf_eq_infi {s : set α} : Inf s = (⨅a ∈ s, a) :=
id                            └─┘     └─┘        
src                           └─┘      └─┘          
typ                           └─┘     └─┘        
doc                                    └─┘           
524  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
525    (le_infi $ assume b, le_infi $ assume h, Inf_le h)
id      └─────┘            └─────┘            └────┘ 
src     └─────┘             └─────┘             └────┘
typ     └─────┘            └─────┘            └────┘ 
526    (le_Inf $ assume b h, infi_le_of_le b $ infi_le _ h)
id      └────┘             └───────────┘    └─────┘   
src     └────┘               └───────────┘     └─────┘
typ     └────┘             └───────────┘    └─────┘   
527  
528  theorem Sup_eq_supr {s : set α} : Sup s = (⨆a ∈ s, a) :=
id                            └─┘     └─┘        
src                           └─┘      └─┘          
typ                           └─┘     └─┘        
doc                                    └─┘           
529  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
530    (Sup_le $ assume b h, le_supr_of_le b $ le_supr _ h)
id      └────┘             └───────────┘    └─────┘   
src     └────┘               └───────────┘     └─────┘
typ     └────┘             └───────────┘    └─────┘   
531    (supr_le $ assume b, supr_le $ assume h, le_Sup h)
id      └─────┘            └─────┘            └────┘ 
src     └─────┘             └─────┘             └────┘
typ     └─────┘            └─────┘            └────┘ 
532  
533  lemma Sup_range {α : Type u} [has_Sup α] {f : ι → α} : Sup (range f) = supr f := rfl
id                                 └─────┘               └─┘  └───┘    └──┘     └─┘
src                                └─────┘                  └─┘  └───┘     └──┘      └─┘
typ                                └─────┘               └─┘  └───┘    └──┘     └─┘
doc                                └─────┘                  └─┘  └───┘      └──┘
534  
535  lemma Inf_range {α : Type u} [has_Inf α] {f : ι → α} : Inf (range f) = infi f := rfl
id                                 └─────┘               └─┘  └───┘    └──┘     └─┘
src                                └─────┘                  └─┘  └───┘     └──┘      └─┘
typ                                └─────┘               └─┘  └───┘    └──┘     └─┘
doc                                └─────┘                  └─┘  └───┘      └──┘
536  
537  lemma supr_range {g : β → α} {f : ι → β} : (⨆b∈range f, g b) = (⨆i, g (f i)) :=
id                                            └───┘           
src                                                └───┘           
typ                                           └───┘           
doc                                                └───┘            
538  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
539    (supr_le $ assume b, supr_le $ assume ⟨i, (h : f i = b)⟩, h ▸ le_supr _ i)
id      └─────┘            └─────┘                           └─────┘
src     └─────┘             └─────┘                                └─────┘
typ     └─────┘            └─────┘                           └─────┘
540    (supr_le $ assume i, le_supr_of_le (f i) $ le_supr (λp, g (f i)) (mem_range_self _))
id      └─────┘            └───────────┘       └─────┘            └────────────┘
src     └─────┘             └───────────┘         └─────┘                └────────────┘
typ     └─────┘            └───────────┘       └─────┘            └────────────┘
541  
542  lemma infi_range {g : β → α} {f : ι → β} : (⨅b∈range f, g b) = (⨅i, g (f i)) :=
id                                            └───┘           
src                                                └───┘           
typ                                           └───┘           
doc                                                └───┘            
543  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
544    (le_infi $ assume i, infi_le_of_le (f i) $ infi_le (λp, g (f i)) (mem_range_self _))
id      └─────┘            └───────────┘       └─────┘            └────────────┘
src     └─────┘             └───────────┘         └─────┘                └────────────┘
typ     └─────┘            └───────────┘       └─────┘            └────────────┘
545    (le_infi $ assume b, le_infi $ assume ⟨i, (h : f i = b)⟩, h ▸ infi_le _ i)
id      └─────┘            └─────┘                           └─────┘
src     └─────┘             └─────┘                                └─────┘
typ     └─────┘            └─────┘                           └─────┘
546  
547  theorem Inf_image {s : set β} {f : β → α} : Inf (f '' s) = (⨅ a ∈ s, f a) :=
id                          └─┘               └─┘   └┘           
src                         └─┘                  └─┘    └┘            
typ                         └─┘               └─┘   └┘           
doc                                              └─┘                   
548  calc Inf (set.image f s) = (⨅a, ⨅h : ∃b, b ∈ s ∧ f b = a, a) : Inf_eq_infi
id        └─┘  └───────┘                         └─────────┘
src       └─┘  └───────┘                                   └─────────┘
typ       └─┘  └───────┘                         └─────────┘
doc       └─┘                                             
549                       ... = (⨅a, ⨅b, ⨅h : f b = a ∧ b ∈ s, a) : by simp [and_comm]
id                                                          └──────┘
src                                                           └────┘└──────┘└─
typ                                                   └────┘└──────┘└─
doc                                                              └────┘        └─
txt                                                                    └────┘        └─
par                                                                    └────┘        └─
pid                                                                                
st                                                                    └────────────────
550                       ... = (⨅a, ⨅b, ⨅h : a = f b, ⨅h : b ∈ s, a) : by simp [infi_and, eq_comm]
id                                                             └──────┘  └─────┘
src  ────────────────────┘                                       └────┘└──────┘└┘└─────┘└─
typ  ────────────────────┘                               └────┘└──────┘└┘└─────┘└─
doc  ────────────────────┘                                         └────┘        └┘       └─
txt  ────────────────────┘                                                 └────┘        └┘       └─
par  ────────────────────┘                                                 └────┘        └┘       └─
pid  ────────────────────┘                                                             └┘       
st   ────────────────────┘                                                └─────────────────────────
551                       ... = (⨅b, ⨅a, ⨅h : a = f b, ⨅h : b ∈ s, a) : by rw [infi_comm]
id                                                           └───────┘
src  ────────────────────┘                                       └──┘└───────┘└─
typ  ────────────────────┘                               └──┘└───────┘└─
doc  ────────────────────┘                                         └──┘         └─
txt  ────────────────────┘                                                 └──┘         └─
par  ────────────────────┘                                                 └──┘         └─
pid  ────────────────────┘                                                   └┘         
st   ────────────────────┘                                                └────────────┘
552                       ... = (⨅a∈s, f a) : congr_arg infi $ by funext x; rw [infi_infi_eq_left]
id                                      └───────┘ └──┘                    └───────────────┘
src  ────────────────────┘                  └───────┘ └──┘      └──────┘  └──┘└───────────────┘└─
typ  ────────────────────┘              └───────┘ └──┘      └──────┘  └──┘└───────────────┘└─
doc  ────────────────────┘                            └──┘      └──────┘  └──┘                 └─
txt  ────────────────────┘                                        └──────┘  └──┘                 └─
par  ────────────────────┘                                        └──────┘  └──┘                 └─
pid  ────────────────────┘                                              └┘    └┘                 
st   ────────────────────┘                                       └─────────────┘└───────────────┘
553  
src  
typ  
doc  
txt  
par  
pid  
st   
554  theorem Sup_image {s : set β} {f : β → α} : Sup (f '' s) = (⨆ a ∈ s, f a) :=
id                          └─┘               └─┘   └┘           
src                         └─┘                  └─┘    └┘            
typ                         └─┘               └─┘   └┘           
doc                                              └─┘                   
555  calc Sup (set.image f s) = (⨆a, ⨆h : ∃b, b ∈ s ∧ f b = a, a) : Sup_eq_supr
id        └─┘  └───────┘                         └─────────┘
src       └─┘  └───────┘                                   └─────────┘
typ       └─┘  └───────┘                         └─────────┘
doc       └─┘                                             
556                       ... = (⨆a, ⨆b, ⨆h : f b = a ∧ b ∈ s, a) : by simp [and_comm]
id                                                          └──────┘
src                                                           └────┘└──────┘└─
typ                                                   └────┘└──────┘└─
doc                                                              └────┘        └─
txt                                                                    └────┘        └─
par                                                                    └────┘        └─
pid                                                                                
st                                                                    └────────────────
557                       ... = (⨆a, ⨆b, ⨆h : a = f b, ⨆h : b ∈ s, a) : by simp [supr_and, eq_comm]
id                                                             └──────┘  └─────┘
src  ────────────────────┘                                       └────┘└──────┘└┘└─────┘└─
typ  ────────────────────┘                               └────┘└──────┘└┘└─────┘└─
doc  ────────────────────┘                                         └────┘        └┘       └─
txt  ────────────────────┘                                                 └────┘        └┘       └─
par  ────────────────────┘                                                 └────┘        └┘       └─
pid  ────────────────────┘                                                             └┘       
st   ────────────────────┘                                                └─────────────────────────
558                       ... = (⨆b, ⨆a, ⨆h : a = f b, ⨆h : b ∈ s, a) : by rw [supr_comm]
id                                                           └───────┘
src  ────────────────────┘                                       └──┘└───────┘└─
typ  ────────────────────┘                               └──┘└───────┘└─
doc  ────────────────────┘                                         └──┘         └─
txt  ────────────────────┘                                                 └──┘         └─
par  ────────────────────┘                                                 └──┘         └─
pid  ────────────────────┘                                                   └┘         
st   ────────────────────┘                                                └────────────┘
559                       ... = (⨆a∈s, f a) : congr_arg supr $ by funext x; rw [supr_supr_eq_left]
id                                      └───────┘ └──┘                    └───────────────┘
src  ────────────────────┘                  └───────┘ └──┘      └──────┘  └──┘└───────────────┘└─
typ  ────────────────────┘              └───────┘ └──┘      └──────┘  └──┘└───────────────┘└─
doc  ────────────────────┘                            └──┘      └──────┘  └──┘                 └─
txt  ────────────────────┘                                        └──────┘  └──┘                 └─
par  ────────────────────┘                                        └──────┘  └──┘                 └─
pid  ────────────────────┘                                              └┘    └┘                 
st   ────────────────────┘                                       └─────────────┘└───────────────┘
560  
src  
typ  
doc  
txt  
par  
pid  
st   
561  /- supr and infi under set constructions -/
src  ────────────────────────────────────────────
typ  ────────────────────────────────────────────
doc  ────────────────────────────────────────────
txt  ────────────────────────────────────────────
par  ────────────────────────────────────────────
pid  ────────────────────────────────────────────
st   ────────────────────────────────────────────
562  
src  
typ  
doc  
txt  
par  
pid  
st   
563  /- should work using the simplifier! -/
src  ───────────────────────────────────────┘
typ  ───────────────────────────────────────┘
doc  ───────────────────────────────────────┘
txt  ───────────────────────────────────────┘
par  ───────────────────────────────────────┘
pid  ───────────────────────────────────────┘
st   ───────────────────────────────────────┘
564  @[simp] theorem infi_emptyset {f : β → α} : (⨅ x ∈ (∅ : set β), f x) = ⊤ :=
id                                                      └─┘       
src                                                        └─┘          
typ                                                     └─┘       
doc    └──┘                                                       
565  le_antisymm le_top (le_infi $ assume x, le_infi false.elim)
id   └─────────┘ └────┘  └─────┘            └─────┘ └────────┘
src  └─────────┘ └────┘  └─────┘             └─────┘ └────────┘
typ  └─────────┘ └────┘  └─────┘            └─────┘ └────────┘
566  
567  @[simp] theorem supr_emptyset {f : β → α} : (⨆ x ∈ (∅ : set β), f x) = ⊥ :=
id                                                      └─┘       
src                                                        └─┘          
typ                                                     └─┘       
doc    └──┘                                                       
568  le_antisymm (supr_le $ assume x, supr_le false.elim) bot_le
id   └─────────┘  └─────┘            └─────┘ └────────┘  └────┘
src  └─────────┘  └─────┘             └─────┘ └────────┘  └────┘
typ  └─────────┘  └─────┘            └─────┘ └────────┘  └────┘
569  
570  @[simp] theorem infi_univ {f : β → α} : (⨅ x ∈ (univ : set β), f x) = (⨅ x, f x) :=
id                                               └──┘   └─┘           
src                                                 └──┘   └─┘             
typ                                              └──┘   └─┘           
doc    └──┘                                                                 
571  show (⨅ (x : β) (H : true), f x) = ⨅ (x : β), f x,
id                      └──┘               
src                      └──┘                
typ                     └──┘               
doc                                           
572    from congr_arg infi $ funext $ assume x, infi_const
id          └───────┘ └──┘   └────┘            └────────┘
src         └───────┘ └──┘   └────┘             └────────┘
typ         └───────┘ └──┘   └────┘            └────────┘
doc                   └──┘
573  
574  @[simp] theorem supr_univ {f : β → α} : (⨆ x ∈ (univ : set β), f x) = (⨆ x, f x) :=
id                                               └──┘   └─┘           
src                                                 └──┘   └─┘             
typ                                              └──┘   └─┘           
doc    └──┘                                                                 
575  show (⨆ (x : β) (H : true), f x) = ⨆ (x : β), f x,
id                      └──┘               
src                      └──┘                
typ                     └──┘               
doc                                           
576    from congr_arg supr $ funext $ assume x, supr_const
id          └───────┘ └──┘   └────┘            └────────┘
src         └───────┘ └──┘   └────┘             └────────┘
typ         └───────┘ └──┘   └────┘            └────────┘
doc                   └──┘
577  
578  @[simp] theorem infi_union {f : β → α} {s t : set β} : (⨅ x ∈ s ∪ t, f x) = (⨅x∈s, f x) ⊓ (⨅x∈t, f x) :=
id                                               └─┘                            
src                                                └─┘                                      
typ                                              └─┘                            
doc    └──┘                                                                                    
579  calc (⨅ x ∈ s ∪ t, f x) = (⨅ x, (⨅h : x∈s, f x) ⊓ (⨅h : x∈t, f x)) : congr_arg infi $ funext $ assume x, infi_or
id                                              └───────┘ └──┘   └────┘            └─────┘
src                                                           └───────┘ └──┘   └────┘             └─────┘
typ                                             └───────┘ └──┘   └────┘            └─────┘
doc                                                                         └──┘
580                      ... = (⨅x∈s, f x) ⊓ (⨅x∈t, f x) : infi_inf_eq
id                                            └─────────┘
src                                                   └─────────┘
typ                                           └─────────┘
doc                                            
581  
582  theorem infi_le_infi_of_subset {f : β → α} {s t : set β} (h : s ⊆ t) :
id                                                   └─┘          
src                                                    └─┘           
typ                                                  └─┘          
583    (⨅ x ∈ t, f x) ≤ (⨅ x ∈ s, f x) :=
id                      
src                         
typ                     
doc                          
584  by rw [(union_eq_self_of_subset_left h).symm, infi_union]; exact inf_le_left
id           └──────────────────────────┘         └────────┘         └─────────┘
src     └──┘ └──────────────────────────┘ └──────┘└────────┘  └────┘└─────────┘
typ     └──┘ └──────────────────────────┘└──────┘└────────┘  └────┘└─────────┘
doc     └──┘                              └──────┘            └────┘           
txt     └──┘                              └──────┘            └────┘           
par     └──┘                              └──────┘            └────┘           
pid       └┘                              └──────┘                            
st     └───────────────────────────────────────┘└───────────┘└───────────────────
585  
src  
typ  
doc  
txt  
par  
pid  
st   
586  @[simp] theorem supr_union {f : β → α} {s t : set β} : (⨆ x ∈ s ∪ t, f x) = (⨆x∈s, f x) ⊔ (⨆x∈t, f x) :=
id                                               └─┘                            
src                                                └─┘                                      
typ                                              └─┘                            
doc    └──┘                                                                                    
587  calc (⨆ x ∈ s ∪ t, f x) = (⨆ x, (⨆h : x∈s, f x) ⊔ (⨆h : x∈t, f x)) : congr_arg supr $ funext $ assume x, supr_or
id                                              └───────┘ └──┘   └────┘            └─────┘
src                                                           └───────┘ └──┘   └────┘             └─────┘
typ                                             └───────┘ └──┘   └────┘            └─────┘
doc                                                                         └──┘
588                      ... = (⨆x∈s, f x) ⊔ (⨆x∈t, f x) : supr_sup_eq
id                                            └─────────┘
src                                                   └─────────┘
typ                                           └─────────┘
doc                                            
589  
590  theorem supr_le_supr_of_subset {f : β → α} {s t : set β} (h : s ⊆ t) :
id                                                   └─┘          
src                                                    └─┘           
typ                                                  └─┘          
591    (⨆ x ∈ s, f x) ≤ (⨆ x ∈ t, f x) :=
id                      
src                         
typ                     
doc                          
592  by rw [(union_eq_self_of_subset_left h).symm, supr_union]; exact le_sup_left
id           └──────────────────────────┘         └────────┘         └─────────┘
src     └──┘ └──────────────────────────┘ └──────┘└────────┘  └────┘└─────────┘
typ     └──┘ └──────────────────────────┘└──────┘└────────┘  └────┘└─────────┘
doc     └──┘                              └──────┘            └────┘           
txt     └──┘                              └──────┘            └────┘           
par     └──┘                              └──────┘            └────┘           
pid       └┘                              └──────┘                            
st     └───────────────────────────────────────┘└───────────┘└───────────────────
593  
src  
typ  
doc  
txt  
par  
pid  
st   
594  @[simp] theorem insert_of_has_insert {α : Type*} (x : α) (a : set α) :
id                                                                └─┘ 
src                                                                └─┘
typ                                                               └─┘ 
doc    └──┘
595    has_insert.insert x a = insert x a := rfl
id     └───────────────┘    └────┘      └─┘
src    └───────────────┘      └────┘        └─┘
typ    └───────────────┘    └────┘      └─┘
596  
597  @[simp] theorem infi_insert {f : β → α} {s : set β} {b : β} : (⨅ x ∈ insert b s, f x) = f b ⊓ (⨅x∈s, f x) :=
id                                              └─┘                 └────┘              
src                                               └─┘                    └────┘                    
typ                                             └─┘                 └────┘              
doc    └──┘                                                                                          
598  eq.trans infi_union $ congr_arg (λx:α, x ⊓ (⨅x∈s, f x)) infi_infi_eq_left
id   └──────┘ └────────┘   └───────┘                └───────────────┘
src  └──────┘ └────────┘   └───────┘                      └───────────────┘
typ  └──────┘ └────────┘   └───────┘                └───────────────┘
doc                                                 
599  
600  @[simp] theorem supr_insert {f : β → α} {s : set β} {b : β} : (⨆ x ∈ insert b s, f x) = f b ⊔ (⨆x∈s, f x) :=
id                                              └─┘                 └────┘              
src                                               └─┘                    └────┘                    
typ                                             └─┘                 └────┘              
doc    └──┘                                                                                          
601  eq.trans supr_union $ congr_arg (λx:α, x ⊔ (⨆x∈s, f x)) supr_supr_eq_left
id   └──────┘ └────────┘   └───────┘                └───────────────┘
src  └──────┘ └────────┘   └───────┘                      └───────────────┘
typ  └──────┘ └────────┘   └───────┘                └───────────────┘
doc                                                 
602  
603  @[simp] theorem infi_singleton {f : β → α} {b : β} : (⨅ x ∈ (singleton b : set β), f x) = f b :=
id                                                           └───────┘    └─┘        
src                                                              └───────┘     └─┘         
typ                                                          └───────┘    └─┘        
doc    └──┘                                                                          
604  show (⨅ x ∈ insert b (∅ : set β), f x) = f b,
id             └────┘      └─┘        
src             └────┘       └─┘         
typ            └────┘      └─┘        
doc                                 
605    by simp
src       └────
typ       └────
doc       └────
txt       └────
par       └────
pid           
st       └─────
606  
src  
typ  
doc  
txt  
par  
pid  
st   
607  @[simp] theorem infi_pair {f : β → α} {a b : β} : (⨅ x ∈ ({a, b} : set β), f x) = f a ⊓ f b :=
id                                                             └─┘           
src                                                                  └─┘              
typ                                                            └─┘           
doc    └──┘                                                                  
608  by { rw [show {a, b} = (insert b {a} : set β), from rfl, infi_insert, inf_comm], simp }
id                          └────┘       └─┘         └─┘  └─────────┘  └──────┘
src       └──┘     └─┘ └┘ └────┘ └───┘└─┘ └──────┘└─┘└┘└─────────┘└┘└──────┘  └───┘
typ       └──┘     └─┘ └┘ └────┘└───┘└─┘└──────┘└─┘└┘└─────────┘└┘└──────┘  └───┘
doc       └──┘     └─┘ └┘          └───┘    └──────┘   └┘           └┘          └───┘
txt       └──┘     └─┘ └┘          └───┘    └──────┘   └┘           └┘          └───┘
par       └──┘     └─┘ └┘          └───┘    └──────┘   └┘           └┘          └───┘
pid         └┘     └─┘ └┘          └───┘    └──────┘   └┘           └┘              
st     └───────────────────────────────────────────────────┘└───────────┘└────────┘└──────┘└┘
609  
610  @[simp] theorem supr_singleton {f : β → α} {b : β} : (⨆ x ∈ (singleton b : set β), f x) = f b :=
id                                                           └───────┘    └─┘        
src                                                              └───────┘     └─┘         
typ                                                          └───────┘    └─┘        
doc    └──┘                                                                          
611  show (⨆ x ∈ insert b (∅ : set β), f x) = f b,
id             └────┘      └─┘        
src             └────┘       └─┘         
typ            └────┘      └─┘        
doc                                 
612    by simp
src       └────
typ       └────
doc       └────
txt       └────
par       └────
pid           
st       └─────
613  
src  
typ  
doc  
txt  
par  
pid  
st   
614  @[simp] theorem supr_pair {f : β → α} {a b : β} : (⨆ x ∈ ({a, b} : set β), f x) = f a ⊔ f b :=
id                                                             └─┘           
src                                                                  └─┘              
typ                                                            └─┘           
doc    └──┘                                                                  
615  by { rw [show {a, b} = (insert b {a} : set β), from rfl, supr_insert, sup_comm], simp }
id                          └────┘       └─┘         └─┘  └─────────┘  └──────┘
src       └──┘     └─┘ └┘ └────┘ └───┘└─┘ └──────┘└─┘└┘└─────────┘└┘└──────┘  └───┘
typ       └──┘     └─┘ └┘ └────┘└───┘└─┘└──────┘└─┘└┘└─────────┘└┘└──────┘  └───┘
doc       └──┘     └─┘ └┘          └───┘    └──────┘   └┘           └┘          └───┘
txt       └──┘     └─┘ └┘          └───┘    └──────┘   └┘           └┘          └───┘
par       └──┘     └─┘ └┘          └───┘    └──────┘   └┘           └┘          └───┘
pid         └┘     └─┘ └┘          └───┘    └──────┘   └┘           └┘              
st     └───────────────────────────────────────────────────┘└───────────┘└────────┘└──────┘└┘
616  
617  lemma infi_image {γ} {f : β → γ} {g : γ → α} {t : set β} :
id                                                 └─┘ 
src                                                    └─┘
typ                                                └─┘ 
618    (⨅ c ∈ f '' t, g c) = (⨅ b ∈ t, g (f b)) :=
id           └┘               
src            └┘                
typ          └┘               
doc                               
619  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
620    (le_infi $ assume b, le_infi $ assume hbt,
id      └─────┘            └─────┘          └─┘
src     └─────┘             └─────┘
typ     └─────┘            └─────┘          └─┘
621      infi_le_of_le (f b) $ infi_le (λ_, g (f b)) (mem_image_of_mem f hbt))
id       └───────────┘       └─────┘            └──────────────┘  └─┘
src      └───────────┘         └─────┘                └──────────────┘
typ      └───────────┘       └─────┘            └──────────────┘  └─┘
622    (le_infi $ assume c, le_infi $ assume ⟨b, hbt, eq⟩,
id      └─────┘            └─────┘            └─┘  └┘
src     └─────┘             └─────┘                   └┘
typ     └─────┘            └─────┘            └─┘  └┘
623      eq ▸ infi_le_of_le b $ infi_le (λ_, g (f b)) hbt)
id           └───────────┘     └─────┘       
src          └───────────┘     └─────┘
typ          └───────────┘     └─────┘       
624  
625  lemma supr_image {γ} {f : β → γ} {g : γ → α} {t : set β} :
id                                                 └─┘ 
src                                                    └─┘
typ                                                └─┘ 
626    (⨆ c ∈ f '' t, g c) = (⨆ b ∈ t, g (f b)) :=
id           └┘               
src            └┘                
typ          └┘               
doc                               
627  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
628    (supr_le $ assume c, supr_le $ assume ⟨b, hbt, eq⟩,
id      └─────┘            └─────┘            └─┘  └┘
src     └─────┘             └─────┘                   └┘
typ     └─────┘            └─────┘            └─┘  └┘
629      eq ▸ le_supr_of_le b $ le_supr (λ_, g (f b)) hbt)
id           └───────────┘     └─────┘       
src          └───────────┘     └─────┘
typ          └───────────┘     └─────┘       
630    (supr_le $ assume b, supr_le $ assume hbt,
id      └─────┘            └─────┘          └─┘
src     └─────┘             └─────┘
typ     └─────┘            └─────┘          └─┘
631      le_supr_of_le (f b) $ le_supr (λ_, g (f b)) (mem_image_of_mem f hbt))
id       └───────────┘       └─────┘            └──────────────┘  └─┘
src      └───────────┘         └─────┘                └──────────────┘
typ      └───────────┘       └─────┘            └──────────────┘  └─┘
632  
633  /- supr and infi under Type -/
634  
635  @[simp] theorem infi_empty {s : empty → α} : infi s = ⊤ :=
id                                   └───┘       └──┘   
src                                  └───┘        └──┘    
typ                                  └───┘       └──┘   
doc    └──┘                                       └──┘
636  le_antisymm le_top (le_infi $ assume i, empty.rec_on _ i)
id   └─────────┘ └────┘  └─────┘            └──────────┘   
src  └─────────┘ └────┘  └─────┘             └──────────┘
typ  └─────────┘ └────┘  └─────┘            └──────────┘   
637  
638  @[simp] theorem supr_empty {s : empty → α} : supr s = ⊥ :=
id                                   └───┘       └──┘   
src                                  └───┘        └──┘    
typ                                  └───┘       └──┘   
doc    └──┘                                       └──┘
639  le_antisymm (supr_le $ assume i, empty.rec_on _ i) bot_le
id   └─────────┘  └─────┘            └──────────┘     └────┘
src  └─────────┘  └─────┘             └──────────┘      └────┘
typ  └─────────┘  └─────┘            └──────────┘     └────┘
640  
641  @[simp] theorem infi_unit {f : unit → α} : (⨅ x, f x) = f () :=
id                                  └──┘               └┘
src                                 └──┘                    └┘
typ                                 └──┘               └┘
doc    └──┘                         └──┘           
642  le_antisymm (infi_le _ _) (le_infi $ assume ⟨⟩, le_refl _)
id   └─────────┘  └─────┘       └─────┘             └─────┘
src  └─────────┘  └─────┘       └─────┘             └─────┘
typ  └─────────┘  └─────┘       └─────┘             └─────┘
643  
644  @[simp] theorem supr_unit {f : unit → α} : (⨆ x, f x) = f () :=
id                                  └──┘               └┘
src                                 └──┘                    └┘
typ                                 └──┘               └┘
doc    └──┘                         └──┘           
645  le_antisymm (supr_le $ assume ⟨⟩, le_refl _) (le_supr _ _)
id   └─────────┘  └─────┘             └─────┘     └─────┘
src  └─────────┘  └─────┘             └─────┘     └─────┘
typ  └─────────┘  └─────┘             └─────┘     └─────┘
646  
647  lemma supr_bool_eq {f : bool → α} : (⨆b:bool, f b) = f tt ⊔ f ff :=
id                           └──┘          └──┘      └┘   └┘
src                          └──┘           └──┘         └┘    └┘
typ                          └──┘          └──┘      └┘   └┘
doc                                             
648  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
649    (supr_le $ assume b, match b with tt := le_sup_left | ff := le_sup_right end)
id      └─────┘                        └┘    └─────────┘   └┘    └──────────┘
src     └─────┘                          └┘    └─────────┘   └┘    └──────────┘
typ     └─────┘                        └┘    └─────────┘   └┘    └──────────┘
650    (sup_le (le_supr _ _) (le_supr _ _))
id      └────┘  └─────┘       └─────┘
src     └────┘  └─────┘       └─────┘
typ     └────┘  └─────┘       └─────┘
651  
652  lemma infi_bool_eq {f : bool → α} : (⨅b:bool, f b) = f tt ⊓ f ff :=
id                           └──┘          └──┘      └┘   └┘
src                          └──┘           └──┘         └┘    └┘
typ                          └──┘          └──┘      └┘   └┘
doc                                             
653  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
654    (le_inf (infi_le _ _) (infi_le _ _))
id      └────┘  └─────┘       └─────┘
src     └────┘  └─────┘       └─────┘
typ     └────┘  └─────┘       └─────┘
655    (le_infi $ assume b, match b with tt := inf_le_left | ff := inf_le_right end)
id      └─────┘                        └┘    └─────────┘   └┘    └──────────┘
src     └─────┘                          └┘    └─────────┘   └┘    └──────────┘
typ     └─────┘                        └┘    └─────────┘   └┘    └──────────┘
656  
657  theorem infi_subtype {p : ι → Prop} {f : subtype p → α} : (⨅ x, f x) = (⨅ i (h:p i), f ⟨i, h⟩) :=
id                                           └─────┘                            
src                                           └─────┘                               
typ                                          └─────┘                            
doc                                                                                  
658  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
659    (le_infi $ assume i, le_infi $ assume : p i, infi_le _ _)
id      └─────┘            └─────┘               └─────┘
src     └─────┘             └─────┘                 └─────┘
typ     └─────┘            └─────┘               └─────┘
660    (le_infi $ assume ⟨i, h⟩, infi_le_of_le i $ infi_le _ _)
id      └─────┘                └───────────┘     └─────┘
src     └─────┘                  └───────────┘     └─────┘
typ     └─────┘                └───────────┘     └─────┘
661  
662  lemma infi_subtype' {p : ι → Prop} {f : ∀ i, p i → α} :
id                                                  
typ                                                 
663    (⨅ i (h : p i), f i h) = (⨅ x : subtype p, f x.val x.property) :=
id                           └─────┘   └──┘ └───────┘
src                                └─────┘      └──┘  └───────┘
typ                          └─────┘   └──┘ └───────┘
doc                                          
664  (@infi_subtype _ _ _ p (λ x, f x.val x.property)).symm
id     └──────────┘              └──┘ └───────┘  └──┘
src    └──────────┘                  └──┘  └───────┘  └──┘
typ    └──────────┘              └──┘ └───────┘  └──┘
665  
666  theorem supr_subtype {p : ι → Prop} {f : subtype p → α} : (⨆ x, f x) = (⨆ i (h:p i), f ⟨i, h⟩) :=
id                                           └─────┘                            
src                                           └─────┘                               
typ                                          └─────┘                            
doc                                                                                  
667  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
668    (supr_le $ assume ⟨i, h⟩, le_supr_of_le i $ le_supr (λh:p i, f ⟨i, h⟩) _)
id      └─────┘                └───────────┘     └─────┘              
src     └─────┘                  └───────────┘     └─────┘
typ     └─────┘                └───────────┘     └─────┘              
669    (supr_le $ assume i, supr_le $ assume : p i, le_supr _ _)
id      └─────┘            └─────┘               └─────┘
src     └─────┘             └─────┘                 └─────┘
typ     └─────┘            └─────┘               └─────┘
670  
671  theorem infi_sigma {p : β → Type w} {f : sigma p → α} : (⨅ x, f x) = (⨅ i (h:p i), f ⟨i, h⟩) :=
id                                           └───┘                            
src                                           └───┘                               
typ                                          └───┘                            
doc                                                                                
672  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
673    (le_infi $ assume i, le_infi $ assume : p i, infi_le _ _)
id      └─────┘            └─────┘               └─────┘
src     └─────┘             └─────┘                 └─────┘
typ     └─────┘            └─────┘               └─────┘
674    (le_infi $ assume ⟨i, h⟩, infi_le_of_le i $ infi_le _ _)
id      └─────┘                └───────────┘     └─────┘
src     └─────┘                  └───────────┘     └─────┘
typ     └─────┘                └───────────┘     └─────┘
675  
676  theorem supr_sigma {p : β → Type w} {f : sigma p → α} : (⨆ x, f x) = (⨆ i (h:p i), f ⟨i, h⟩) :=
id                                           └───┘                            
src                                           └───┘                               
typ                                          └───┘                            
doc                                                                                
677  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
678    (supr_le $ assume ⟨i, h⟩, le_supr_of_le i $ le_supr (λh:p i, f ⟨i, h⟩) _)
id      └─────┘                └───────────┘     └─────┘              
src     └─────┘                  └───────────┘     └─────┘
typ     └─────┘                └───────────┘     └─────┘              
679    (supr_le $ assume i, supr_le $ assume : p i, le_supr _ _)
id      └─────┘            └─────┘               └─────┘
src     └─────┘             └─────┘                 └─────┘
typ     └─────┘            └─────┘               └─────┘
680  
681  theorem infi_prod {γ : Type w} {f : β × γ → α} : (⨅ x, f x) = (⨅ i j, f (i, j)) :=
id                                                              
src                                                                    
typ                                                             
doc                                                                   
682  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
683    (le_infi $ assume i, le_infi $ assume j, infi_le _ _)
id      └─────┘            └─────┘            └─────┘
src     └─────┘             └─────┘             └─────┘
typ     └─────┘            └─────┘            └─────┘
684    (le_infi $ assume ⟨i, h⟩, infi_le_of_le i $ infi_le _ _)
id      └─────┘                └───────────┘     └─────┘
src     └─────┘                  └───────────┘     └─────┘
typ     └─────┘                └───────────┘     └─────┘
685  
686  theorem supr_prod {γ : Type w} {f : β × γ → α} : (⨆ x, f x) = (⨆ i j, f (i, j)) :=
id                                                              
src                                                                    
typ                                                             
doc                                                                   
687  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
688    (supr_le $ assume ⟨i, h⟩, le_supr_of_le i $ le_supr (λj, f ⟨i, j⟩) _)
id      └─────┘                └───────────┘     └─────┘          
src     └─────┘                  └───────────┘     └─────┘
typ     └─────┘                └───────────┘     └─────┘          
689    (supr_le $ assume i, supr_le $ assume j, le_supr _ _)
id      └─────┘            └─────┘            └─────┘
src     └─────┘             └─────┘             └─────┘
typ     └─────┘            └─────┘            └─────┘
690  
691  theorem infi_sum {γ : Type w} {f : β ⊕ γ → α} :
id                                           
src                                       
typ                                          
692    (⨅ x, f x) = (⨅ i, f (sum.inl i)) ⊓ (⨅ j, f (sum.inr j)) :=
id                 └─────┘          └─────┘ 
src                     └─────┘             └─────┘
typ                └─────┘          └─────┘ 
doc                                       
693  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
694    (le_inf
id      └────┘
src     └────┘
typ     └────┘
695      (infi_le_infi2 $ assume i, ⟨_, le_refl _⟩)
id        └───────────┘                └─────┘
src       └───────────┘                 └─────┘
typ       └───────────┘                └─────┘
696      (infi_le_infi2 $ assume j, ⟨_, le_refl _⟩))
id        └───────────┘                └─────┘
src       └───────────┘                 └─────┘
typ       └───────────┘                └─────┘
697    (le_infi $ assume s, match s with
id      └─────┘                  
src     └─────┘
typ     └─────┘                  
698    | sum.inl i := inf_le_left_of_le $ infi_le _ _
id       └─────┘      └───────────────┘   └─────┘
src      └─────┘      └───────────────┘   └─────┘
typ      └─────┘      └───────────────┘   └─────┘
699    | sum.inr j := inf_le_right_of_le $ infi_le _ _
id       └─────┘      └────────────────┘   └─────┘
src      └─────┘      └────────────────┘   └─────┘
typ      └─────┘      └────────────────┘   └─────┘
700    end)
701  
702  theorem supr_sum {γ : Type w} {f : β ⊕ γ → α} :
id                                           
src                                       
typ                                          
703    (⨆ x, f x) = (⨆ i, f (sum.inl i)) ⊔ (⨆ j, f (sum.inr j)) :=
id                 └─────┘          └─────┘ 
src                     └─────┘             └─────┘
typ                └─────┘          └─────┘ 
doc                                       
704  le_antisymm
id   └─────────┘
src  └─────────┘
typ  └─────────┘
705    (supr_le $ assume s, match s with
id      └─────┘                  
src     └─────┘
typ     └─────┘                  
706    | sum.inl i := le_sup_left_of_le $ le_supr _ i
id       └─────┘     └───────────────┘   └─────┘
src      └─────┘      └───────────────┘   └─────┘
typ      └─────┘     └───────────────┘   └─────┘
707    | sum.inr j := le_sup_right_of_le $ le_supr _ j
id       └─────┘     └────────────────┘   └─────┘
src      └─────┘      └────────────────┘   └─────┘
typ      └─────┘     └────────────────┘   └─────┘
708    end)
709    (sup_le
id      └────┘
src     └────┘
typ     └────┘
710      (supr_le_supr2 $ assume i, ⟨sum.inl i, le_refl _⟩)
id        └───────────┘             └─────┘   └─────┘
src       └───────────┘              └─────┘    └─────┘
typ       └───────────┘             └─────┘   └─────┘
711      (supr_le_supr2 $ assume j, ⟨sum.inr j, le_refl _⟩))
id        └───────────┘             └─────┘   └─────┘
src       └───────────┘              └─────┘    └─────┘
typ       └───────────┘             └─────┘   └─────┘
712  
713  end
714  
715  section complete_linear_order
716  variables [complete_linear_order α]
id              └───────────────────┘
src             └───────────────────┘
typ             └───────────────────┘
doc             └───────────────────┘
717  
718  lemma supr_eq_top (f : ι → α) : supr f = ⊤ ↔ (∀b<⊤, ∃i, b < f i) :=
id                                 └──┘              
src                                  └──┘                
typ                                └──┘              
doc                                  └──┘
719  by rw [← Sup_range, Sup_eq_top];
id            └───────┘  └────────┘
src     └────┘└───────┘└┘└────────┘
typ     └────┘└───────┘└┘└────────┘
doc     └────┘         └┘          
txt     └────┘         └┘          
par     └────┘         └┘          
pid       └──┘         └┘          
st     └──────────────┘└──────────┘└─
720  from forall_congr (assume b, forall_congr (assume hb, set.exists_range_iff))
id                                └──────────┘             └──────────────────┘
src  └───┘                   └──┘└──────────┘       └───┘└──────────────────┘└──
typ  └───┘                   └──┘└──────────┘       └───┘└──────────────────┘└──
doc  └───┘                   └──┘                   └───┘                    └──
txt  └───┘                   └──┘                   └───┘                    └──
par  └───┘                   └──┘                   └───┘                    └──
pid  └───┘                   └──┘                   └───┘                    └┘
st   ─────────────────────────────────────────────────────────────────────────────
721  
src  
typ  
doc  
txt  
par  
pid  
st   
722  lemma infi_eq_bot (f : ι → α) : infi f = ⊥ ↔ (∀b>⊥, ∃i, b > f i) :=
id                                 └──┘              
src                                  └──┘                
typ                                └──┘              
doc                                  └──┘
723  by rw [← Inf_range, Inf_eq_bot];
id            └───────┘  └────────┘
src     └────┘└───────┘└┘└────────┘
typ     └────┘└───────┘└┘└────────┘
doc     └────┘         └┘          
txt     └────┘         └┘          
par     └────┘         └┘          
pid       └──┘         └┘          
st     └──────────────┘└──────────┘└─
724  from forall_congr (assume b, forall_congr (assume hb, set.exists_range_iff))
id                                └──────────┘             └──────────────────┘
src  └───┘                   └──┘└──────────┘       └───┘└──────────────────┘└──
typ  └───┘                   └──┘└──────────┘       └───┘└──────────────────┘└──
doc  └───┘                   └──┘                   └───┘                    └──
txt  └───┘                   └──┘                   └───┘                    └──
par  └───┘                   └──┘                   └───┘                    └──
pid  └───┘                   └──┘                   └───┘                    └┘
st   ─────────────────────────────────────────────────────────────────────────────
725  
src  
typ  
doc  
txt  
par  
pid  
st   
726  end complete_linear_order
727  
728  /- Instances -/
729  
730  instance complete_lattice_Prop : complete_lattice Prop :=
id                                    └──────────────┘
src                                   └──────────────┘
typ                                   └──────────────┘
doc                                   └──────────────┘
731  { Sup    := λs, ∃a∈s, a,
id                    
src                     
typ                   
732    le_Sup := assume s a h p, ⟨a, h, p⟩,
id                                
typ                               
733    Sup_le := assume s a h ⟨b, h', p⟩, h b h' p,
id                            └┘     
typ                           └┘     
734    Inf    := λs, ∀a:Prop, a∈s → a,
id                     └──┘     
src                            
typ                    └──┘     
735    Inf_le := assume s a h p, p a h,
id                             
typ                            
736    le_Inf := assume s a h p b hb, h b hb p,
id                           └┘    └┘ 
typ                          └┘    └┘ 
737    ..lattice.bounded_lattice_Prop }
id       └──────────────────────────┘
src      └──────────────────────────┘
typ      └──────────────────────────┘
738  
739  lemma Inf_Prop_eq {s : set Prop} : Inf s = (∀p ∈ s, p) := rfl
id                          └─┘         └─┘               └─┘
src                         └─┘         └─┘                   └─┘
typ                         └─┘         └─┘               └─┘
doc                                     └─┘
740  
741  lemma Sup_Prop_eq {s : set Prop} : Sup s = (∃p ∈ s, p) := rfl
id                          └─┘         └─┘             └─┘
src                         └─┘         └─┘                 └─┘
typ                         └─┘         └─┘             └─┘
doc                                     └─┘
742  
743  lemma infi_Prop_eq {ι : Sort*} {p : ι → Prop} : (⨅i, p i) = (∀i, p i) :=
id                                                             
src                                                          
typ                                                            
doc                                                    
744  le_antisymm (assume h i, h _ ⟨i, rfl⟩ ) (assume h p ⟨i, eq⟩, eq ▸ h i)
id   └─────────┘                  └─┘                └┘       
src  └─────────┘                      └─┘                    └┘      
typ  └─────────┘                  └─┘                └┘       
745  
746  lemma supr_Prop_eq {ι : Sort*} {p : ι → Prop} : (⨆i, p i) = (∃i, p i) :=
id                                                           
src                                                             
typ                                                          
doc                                                    
747  le_antisymm (assume ⟨q, ⟨i, (eq : p i = q)⟩, hq⟩, ⟨i, eq.symm ▸ hq⟩) (assume ⟨i, hi⟩, ⟨p i, ⟨i, rfl⟩, hi⟩)
id   └─────────┘                             └┘         └───┘                 └┘            └─┘
src  └─────────┘                                           └───┘                                  └─┘
typ  └─────────┘                             └┘         └───┘                 └┘            └─┘
748  
749  instance pi.complete_lattice {α : Type u} {β : α → Type v} [∀ i, complete_lattice (β i)] :
id                                                                  └──────────────┘   
src                                                                   └──────────────┘
typ                                                                 └──────────────┘   
doc                                                                   └──────────────┘
750    complete_lattice (Π i, β i) :=
id     └──────────────┘       
src    └──────────────┘
typ    └──────────────┘       
doc    └──────────────┘
751  by { pi_instance;
src       └─────────┘
typ       └─────────┘
txt       └─────────┘
par       └─────────┘
st     └───────────────
752       { intros, intro,
src         └────┘  └───┘
typ         └────┘  └───┘
doc         └────┘  └───┘
txt         └────┘  └───┘
par         └────┘  └───┘
st   ────┘└──────┘└─────┘└─
753         apply_field, intros,
src         └─────────┘  └────┘
typ         └─────────┘  └────┘
doc         └─────────┘  └────┘
txt         └─────────┘  └────┘
par         └─────────┘  └────┘
st   ─────────────────┘└──────┘└─
754         simp at H, rcases H with ⟨ x, H₀, H₁ ⟩,
id                            
src         └───────┘  └─────┘ └─────────────────┘
typ         └───────┘  └─────┘└─────────────────┘
doc         └───────┘  └─────┘ └─────────────────┘
txt         └───────┘  └─────┘ └─────────────────┘
par         └───────┘  └─────┘ └─────────────────┘
pid             └──┘         └─────────────────┘
st   ───────────────┘└───────────────────────────┘└─
755         subst b, apply a_1 _ H₀ i, } }
id                        └─┘   └┘ 
src         └────┘   └────┘   └─┘  
typ         └────┘  └────┘└─┘└─┘└┘
doc         └────┘   └────┘   └─┘  
txt         └────┘   └────┘   └─┘  
par         └────┘   └────┘   └─┘  
pid                         └─┘  
st   ─────────────┘└────────────────┘└────┘
756  
757  lemma Inf_apply
758    {α : Type u} {β : α → Type v} [∀ i, complete_lattice (β i)] {s : set (Πa, β a)} {a : α} :
id                                       └──────────────┘           └─┘              
src                                        └──────────────┘             └─┘
typ                                      └──────────────┘           └─┘              
doc                                        └──────────────┘
759    (Inf s) a = (⨅f∈s, (f : Πa, β a) a) :=
id      └─┘                  
src     └─┘           
typ     └─┘                  
doc     └─┘            
760  by rw [← Inf_image]; refl
id            └───────┘
src     └────┘└───────┘  └────
typ     └────┘└───────┘  └────
doc     └────┘           └────
txt     └────┘           └────
par     └────┘           └────
pid       └──┘               
st     └──────────────┘└──────
761  
src  
typ  
doc  
txt  
par  
pid  
st   
762  lemma infi_apply {α : Type u} {β : α → Type v} {ι : Sort*} [∀ i, complete_lattice (β i)]
id                                                                  └──────────────┘   
src                                                                   └──────────────┘
typ                                                                 └──────────────┘   
doc                                                                   └──────────────┘
763    {f : ι → Πa, β a} {a : α} : (⨅i, f i) a = (⨅i, f i a) :=
id                                       
src                                             
typ                                      
doc                                              
764  by erw [← Inf_range, Inf_apply, infi_range]
id             └───────┘  └───────┘  └────────┘
src     └─────┘└───────┘└┘└───────┘└┘└────────┘└─
typ     └─────┘└───────┘└┘└───────┘└┘└────────┘└─
doc     └─────┘         └┘         └┘          └─
txt     └─────┘         └┘         └┘          └─
par     └─────┘         └┘         └┘          └─
pid        └──┘         └┘         └┘          
st     └───────────────┘└─────────┘└──────────┘
765  
src  
typ  
doc  
txt  
par  
pid  
st   
766  lemma Sup_apply
767    {α : Type u} {β : α → Type v} [∀ i, complete_lattice (β i)] {s : set (Πa, β a)} {a : α} :
id                                       └──────────────┘           └─┘              
src                                        └──────────────┘             └─┘
typ                                      └──────────────┘           └─┘              
doc                                        └──────────────┘
768    (Sup s) a = (⨆f∈s, (f : Πa, β a) a) :=
id      └─┘                  
src     └─┘           
typ     └─┘                  
doc     └─┘            
769  by rw [← Sup_image]; refl
id            └───────┘
src     └────┘└───────┘  └────
typ     └────┘└───────┘  └────
doc     └────┘           └────
txt     └────┘           └────
par     └────┘           └────
pid       └──┘               
st     └──────────────┘└──────
770  
src  
typ  
doc  
txt  
par  
pid  
st   
771  lemma supr_apply {α : Type u} {β : α → Type v} {ι : Sort*} [∀ i, complete_lattice (β i)]
id                                                                  └──────────────┘   
src                                                                   └──────────────┘
typ                                                                 └──────────────┘   
doc                                                                   └──────────────┘
772    {f : ι → Πa, β a} {a : α} : (⨆i, f i) a = (⨆i, f i a) :=
id                                       
src                                             
typ                                      
doc                                              
773  by erw [← Sup_range, Sup_apply, supr_range]
id             └───────┘  └───────┘  └────────┘
src     └─────┘└───────┘└┘└───────┘└┘└────────┘└─
typ     └─────┘└───────┘└┘└───────┘└┘└────────┘└─
doc     └─────┘         └┘         └┘          └─
txt     └─────┘         └┘         └┘          └─
par     └─────┘         └┘         └┘          └─
pid        └──┘         └┘         └┘          
st     └───────────────┘└─────────┘└──────────┘
774  
src  
typ  
doc  
txt  
par  
pid  
st   
775  section complete_lattice
776  variables [preorder α] [complete_lattice β]
id              └──────┘     └──────────────┘
src             └──────┘     └──────────────┘
typ             └──────┘     └──────────────┘
doc                          └──────────────┘
777  
778  theorem monotone_Sup_of_monotone {s : set (α → β)} (m_s : ∀f∈s, monotone f) : monotone (Sup s) :=
id                                         └─┘                   └──────┘     └──────┘  └─┘ 
src                                        └─┘                       └──────┘      └──────┘  └─┘
typ                                        └─┘                   └──────┘     └──────┘  └─┘ 
doc                                                                  └──────┘      └──────┘  └─┘
779  assume x y h, Sup_le $ assume x' ⟨f, f_in, fx_eq⟩, le_Sup_of_le ⟨f, f_in, rfl⟩ $ fx_eq ▸ m_s _ f_in h
id              └────┘          └┘   └──┘  └───┘   └──────────┘           └─┘           └─┘        
src                └────┘                               └──────────┘           └─┘          
typ             └────┘          └┘   └──┘  └───┘   └──────────┘           └─┘           └─┘        
780  
781  theorem monotone_Inf_of_monotone {s : set (α → β)} (m_s : ∀f∈s, monotone f) : monotone (Inf s) :=
id                                         └─┘                   └──────┘     └──────┘  └─┘ 
src                                        └─┘                       └──────┘      └──────┘  └─┘
typ                                        └─┘                   └──────┘     └──────┘  └─┘ 
doc                                                                  └──────┘      └──────┘  └─┘
782  assume x y h, le_Inf $ assume x' ⟨f, f_in, fx_eq⟩, Inf_le_of_le ⟨f, f_in, rfl⟩ $ fx_eq ▸ m_s _ f_in h
id              └────┘          └┘   └──┘  └───┘   └──────────┘           └─┘           └─┘        
src                └────┘                               └──────────┘           └─┘          
typ             └────┘          └┘   └──┘  └───┘   └──────────┘           └─┘           └─┘        
783  
784  end complete_lattice
785  
786  section ord_continuous
787  open lattice
788  variables [complete_lattice α] [complete_lattice β]
id              └──────────────┘     └──────────────┘
src             └──────────────┘     └──────────────┘
typ             └──────────────┘     └──────────────┘
doc             └──────────────┘     └──────────────┘
789  
790  /-- A function `f` between complete lattices is order-continuous
791    if it preserves all suprema. -/
792  def ord_continuous (f : α → β) := ∀s : set α, f (Sup s) = (⨆i∈s, f i)
id                                        └─┘     └─┘        
src                                         └─┘       └─┘         
typ                                       └─┘     └─┘        
doc                                                   └─┘          
793  
794  lemma ord_continuous_sup {f : α → β} {a₁ a₂ : α} (hf : ord_continuous f) : f (a₁ ⊔ a₂) = f a₁ ⊔ f a₂ :=
id                                                       └────────────┘       └┘  └┘    └┘   └┘
src                                                         └────────────┘                       
typ                                                      └────────────┘       └┘  └┘    └┘   └┘
doc                                                         └────────────┘
795  have h : f (Sup {a₁, a₂}) = (⨆i∈({a₁, a₂} : set α), f i), from hf _,
id              └─┘ └┘ └┘       └┘ └┘    └─┘            └┘
src              └─┘                       └─┘   
typ             └─┘ └┘ └┘       └┘ └┘    └─┘            └┘
doc              └─┘                                  
796  have h₁ : {a₁, a₂} = (insert a₂ {a₁} : set α), from rfl,
id             └┘ └┘    └────┘ └┘ └┘    └─┘         └─┘
src                     └────┘          └─┘          └─┘
typ            └┘ └┘    └────┘ └┘ └┘    └─┘         └─┘
797  begin
st   └─────
798    rw [h₁, Sup_insert, Sup_singleton, sup_comm] at h,
id         └┘  └────────┘  └───────────┘  └──────┘
src    └──┘  └┘└────────┘└┘└───────────┘└┘└──────┘└────┘
typ    └──┘└┘└┘└────────┘└┘└───────────┘└┘└──────┘└────┘
doc    └──┘  └┘          └┘             └┘        └────┘
txt    └──┘  └┘          └┘             └┘        └────┘
par    └──┘  └┘          └┘             └┘        └────┘
pid      └┘  └┘          └┘             └┘        └───┘
st   ───────┘└──────────┘└─────────────┘└────────┘└───┘└─
799    rw [h, supr_insert, supr_singleton, sup_comm]
id           └─────────┘  └────────────┘  └──────┘
src    └──┘ └┘└─────────┘└┘└────────────┘└┘└──────┘└┘
typ    └──┘└┘└─────────┘└┘└────────────┘└┘└──────┘└┘
doc    └──┘ └┘           └┘              └┘        └┘
txt    └──┘ └┘           └┘              └┘        └┘
par    └──┘ └┘           └┘              └┘        └┘
pid      └┘ └┘           └┘              └┘        
st   ──────┘└───────────┘└──────────────┘└────────┘
800  end
st   └─┘
801  
802  lemma ord_continuous_mono {f : α → β} (hf : ord_continuous f) : monotone f :=
id                                             └────────────┘     └──────┘ 
src                                              └────────────┘      └──────┘
typ                                            └────────────┘     └──────┘ 
doc                                              └────────────┘      └──────┘
803  assume a₁ a₂ h,
id          └┘ └┘ 
typ         └┘ └┘ 
804  calc f a₁ ≤ f a₁ ⊔ f a₂ : le_sup_left
id         └┘    └┘   └┘   └─────────┘
src                           └─────────┘
typ        └┘    └┘   └┘   └─────────┘
805    ... = f (a₁ ⊔ a₂) : (ord_continuous_sup hf).symm
id             └┘  └┘     └────────────────┘ └┘ └──┘
src                        └────────────────┘    └──┘
typ            └┘  └┘     └────────────────┘ └┘ └──┘
806    ... = _ : by rw [sup_of_le_right h]
id                      └─────────────┘ 
src                 └──┘└─────────────┘ └─
typ                 └──┘└─────────────┘└─
doc                 └──┘                └─
txt                 └──┘                └─
par                 └──┘                └─
pid                   └┘                
st                 └────────────────────┘
807  
src  
typ  
doc  
txt  
par  
pid  
st   
808  end ord_continuous
809  end lattice
810  
811  namespace order_dual
812  open lattice
813  variable (α : Type*)
814  
815  instance [has_Inf α] : has_Sup (order_dual α) := ⟨(Inf : set α → α)⟩
id             └─────┘     └─────┘  └────────┘        └─┘   └─┘    
src            └─────┘      └─────┘  └────────┘         └─┘   └─┘
typ            └─────┘     └─────┘  └────────┘        └─┘   └─┘    
doc            └─────┘      └─────┘  └────────┘         └─┘
816  instance [has_Sup α] : has_Inf (order_dual α) := ⟨(Sup : set α → α)⟩
id             └─────┘     └─────┘  └────────┘        └─┘   └─┘    
src            └─────┘      └─────┘  └────────┘         └─┘   └─┘
typ            └─────┘     └─────┘  └────────┘        └─┘   └─┘    
doc            └─────┘      └─────┘  └────────┘         └─┘
817  
818  instance [complete_lattice α] : complete_lattice (order_dual α) :=
id             └──────────────┘     └──────────────┘  └────────┘ 
src            └──────────────┘      └──────────────┘  └────────┘
typ            └──────────────┘     └──────────────┘  └────────┘ 
doc            └──────────────┘      └──────────────┘  └────────┘
819  { le_Sup := @complete_lattice.Inf_le α _,
id                └─────────────────────┘ 
src               └─────────────────────┘
typ               └─────────────────────┘ 
820    Sup_le := @complete_lattice.le_Inf α _,
id                └─────────────────────┘ 
src               └─────────────────────┘
typ               └─────────────────────┘ 
821    Inf_le := @complete_lattice.le_Sup α _,
id                └─────────────────────┘ 
src               └─────────────────────┘
typ               └─────────────────────┘ 
822    le_Inf := @complete_lattice.Sup_le α _,
id                └─────────────────────┘ 
src               └─────────────────────┘
typ               └─────────────────────┘ 
823    .. order_dual.lattice.bounded_lattice α, ..order_dual.lattice.has_Sup α, ..order_dual.lattice.has_Inf α }
id        └────────────────────────────────┘     └────────────────────────┘     └────────────────────────┘ 
src       └────────────────────────────────┘      └────────────────────────┘      └────────────────────────┘
typ       └────────────────────────────────┘     └────────────────────────┘     └────────────────────────┘ 
824  
825  instance [complete_linear_order α] : complete_linear_order (order_dual α) :=
id             └───────────────────┘     └───────────────────┘  └────────┘ 
src            └───────────────────┘      └───────────────────┘  └────────┘
typ            └───────────────────┘     └───────────────────┘  └────────┘ 
doc            └───────────────────┘      └───────────────────┘  └────────┘
826  { .. order_dual.lattice.complete_lattice α, .. order_dual.decidable_linear_order α }
id        └─────────────────────────────────┘      └───────────────────────────────┘ 
src       └─────────────────────────────────┘       └───────────────────────────────┘
typ       └─────────────────────────────────┘      └───────────────────────────────┘ 
827  
828  end order_dual
829  
830  namespace prod
831  open lattice
832  variables (α : Type*) (β : Type*)
833  
834  instance [has_Inf α] [has_Inf β] : has_Inf (α × β) :=
id             └─────┘    └─────┘     └─────┘    
src            └─────┘     └─────┘      └─────┘    
typ            └─────┘    └─────┘     └─────┘    
doc            └─────┘     └─────┘      └─────┘
835  ⟨λs, (Inf (prod.fst '' s), Inf (prod.snd '' s))⟩
id       └─┘  └──────┘ └┘    └─┘  └──────┘ └┘ 
src       └─┘  └──────┘ └┘     └─┘  └──────┘ └┘
typ      └─┘  └──────┘ └┘    └─┘  └──────┘ └┘ 
doc        └─┘                  └─┘
836  
837  instance [has_Sup α] [has_Sup β] : has_Sup (α × β) :=
id             └─────┘    └─────┘     └─────┘    
src            └─────┘     └─────┘      └─────┘    
typ            └─────┘    └─────┘     └─────┘    
doc            └─────┘     └─────┘      └─────┘
838  ⟨λs, (Sup (prod.fst '' s), Sup (prod.snd '' s))⟩
id       └─┘  └──────┘ └┘    └─┘  └──────┘ └┘ 
src       └─┘  └──────┘ └┘     └─┘  └──────┘ └┘
typ      └─┘  └──────┘ └┘    └─┘  └──────┘ └┘ 
doc        └─┘                  └─┘
839  
840  instance [complete_lattice α] [complete_lattice β] : complete_lattice (α × β) :=
id             └──────────────┘    └──────────────┘     └──────────────┘    
src            └──────────────┘     └──────────────┘      └──────────────┘    
typ            └──────────────┘    └──────────────┘     └──────────────┘    
doc            └──────────────┘     └──────────────┘      └──────────────┘
841  { le_Sup := assume s p hab, ⟨le_Sup $ mem_image_of_mem _ hab, le_Sup $ mem_image_of_mem _ hab⟩,
id                        └─┘   └────┘   └──────────────┘   └─┘  └────┘   └──────────────┘   └─┘
src                               └────┘   └──────────────┘        └────┘   └──────────────┘
typ                       └─┘   └────┘   └──────────────┘   └─┘  └────┘   └──────────────┘   └─┘
842    Sup_le := assume s p h,
id                        
typ                       
843      ⟨ Sup_le $ ball_image_of_ball $ assume p hp, (h p hp).1,
id         └────┘   └────────────────┘           └┘     └┘ 
src        └────┘   └────────────────┘                        
typ        └────┘   └────────────────┘           └┘     └┘ 
844        Sup_le $ ball_image_of_ball $ assume p hp, (h p hp).2⟩,
id         └────┘   └────────────────┘           └┘     └┘ 
src        └────┘   └────────────────┘                        
typ        └────┘   └────────────────┘           └┘     └┘ 
845    Inf_le := assume s p hab, ⟨Inf_le $ mem_image_of_mem _ hab, Inf_le $ mem_image_of_mem _ hab⟩,
id                        └─┘   └────┘   └──────────────┘   └─┘  └────┘   └──────────────┘   └─┘
src                               └────┘   └──────────────┘        └────┘   └──────────────┘
typ                       └─┘   └────┘   └──────────────┘   └─┘  └────┘   └──────────────┘   └─┘
846    le_Inf := assume s p h,
id                        
typ                       
847      ⟨ le_Inf $ ball_image_of_ball $ assume p hp, (h p hp).1,
id         └────┘   └────────────────┘           └┘     └┘ 
src        └────┘   └────────────────┘                        
typ        └────┘   └────────────────┘           └┘     └┘ 
848        le_Inf $ ball_image_of_ball $ assume p hp, (h p hp).2⟩,
id         └────┘   └────────────────┘           └┘     └┘ 
src        └────┘   └────────────────┘                        
typ        └────┘   └────────────────┘           └┘     └┘ 
849    .. prod.lattice.bounded_lattice α β,
id        └──────────────────────────┘  
src       └──────────────────────────┘
typ       └──────────────────────────┘  
850    .. prod.lattice.has_Sup α β,
id        └──────────────────┘  
src       └──────────────────┘
typ       └──────────────────┘  
851    .. prod.lattice.has_Inf α β }
id        └──────────────────┘  
src       └──────────────────┘
typ       └──────────────────┘  
852  
853  end prod